Radu Grosu

Rank/Position Title:

Assistant Professor

Home Page:

http://www.cs.sunysb.edu/~grosu

Date of original appointment to this faculty, followed by dates and ranks of advancement:

8/01/2000

Degrees:

Conferences, workshops, and professional development:

Teaching Assistant for the course "Improving the Communication Skills of Computer Scientists", Fall 1997, TU Munich, Germany.

Other related computing experience:

• October 1998 - July 2000: Research Associate, Dept. of CIS, University of Pennsylvania , USA .
• June 1995 - September 1998: Scientific Assistant, Dept. of CS, TU of Munich , Germany .
• July 1990 - May 1995: Scientific Researcher, Dept. of CS, TU of Munich , Germany .
• October 1986 - June 1990: System Engineer, Electronic Computing Center of Cluj , Romania .

Department, college, and/or university committee membership:

• Undergraduate Recruiting Committee.
• PhD Qualifying Examination Committee.

Principal publications of the last five years.

• R. Alur, R. Grosu, I. Lee, O. Sokolsky. Compositional Modeling and Refinement for Hierarchical Hybrid Systems. The Journal of Algebraic and Logic Programming - Special Issue on Process Theory and Hybrid Systems. In print.
• R. Grosu, S.A. Smolka. Safety-Liveness Semantics for UML 2.0 Sequence Diagrams. In Proceedings of ACSD 2005, the 5 th International Conference on Application of Concurrency to System Design. St Malo, France, June 2005.
• R. Grosu, S.A. Smolka. Monte Carlo Model Checking. In Proceedings of TACAS 2005, the 11 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Edinburgh, U.K., April, 2005, p. 271, LNCS 3440.
• P. Ye, E. Entcheva, R. Grosu, S.A. Smolka. Efficient Modeling of Excitable Cells using Hybrid Automata. In Proceedings of CMSB, Computational Methods in Systems Biology Workshop, Edinburgh, Scotland, April, 2005, p. 216.
• R. Grosu, S.A. Smolka. Quantitative Model Checking. In Proceedings of ISoLA , the 1 st International Symposium on Leveraging Applications of Formal Methods, Pahphos, Cyprus, November 2004, p. 165, 2004.
• R. Grosu, X. Huang, S.A. Smolka, P. Yang. Monte Carlo Analysis of Security Protocols: Needham-Schroeder Revisited. In Proceedings of the DIMACS Workshop on Security Analysis of Protocols, Rutgers University, June 2004.
• R. Alur, R. Grosu. Modular Refinement of Hierarchic Reactive Machines. ACM Transactions on Programming Languages and Systems (TOPLAS), p.339, vol. 25, (2004).
• M. Broy, R. Grosu, I. Krüger. Automatically Generating A Program. US Patent No.: 06405361, 2002.
• R. Grosu, T. Stauner. Modular and Visual Specification of Hybrid Systems - An Introduction to HyCharts. Formal Methods in System Design 21(1), Kluwer Academic Publishers, 2002.
• R. Grosu, E. Zadok, S.A. Smolka, R. Cleaveland, Y.A. Liu. HighConfidence Operating Systems. In Proc. of EW'02, the 10th ACM SIGOPS European Workshop "Can we really depend on an OS, 22nd - 25th September 2002, Saint-Emilion , France .

Other scholarly activity: grants, sabbaticals, software development, etc.:

• REUTERS award SPIR-27656, Translator of BizletL to BPEL4WS and Model Checker for BizletL, 6/1/2002 - 5/31/2003, $20,000 (with A. Bernstein and P. Lewis).
• REUTERS award SPIR-27658, Correctness Checker and Automatic Generator of BizletL Workflows, 6/1/2002 - 5/31/2003, $20,000 (with A. Bernstein and P. Lewis).
• BMR award Br 887/12-1, InTime - Methodological Founded Development of Real-Time Systems, 2/1/2000 - 1/1/2003, Euro 226,023 (with M. Broy).
• NATO award HTECH.CRG97-2948, Dynamic Dataflow Networks, 7/1/1998 - 6/30/2000, DM 225,000 (with M. Broy and G. Stefanescu).
• DFG award ITS-9001-C2, SPECTRUM - Deduction oriented Specification and Design of Software, 1/1/90 -- 12/31/93 , DM 1,782,400 (with M. Broy and M. Wirsing).
• Developed jMocha Model Checker. Url: http://www.cs.sunysb.edu/~mocha Developed Charon Simulator. Url: http://www.cis.upenn.edu/mobies/charon/ Developed GMC Model Checker. Url: http://www.cs.sunysb.edu/~gmc

Scientific, professional, and honor societies of which you are a member:

ACM, GI.

Honors and awards:

NSF CAREER award CCR01-33583, Model-Based Design and Verification of Embedded Systems, 6/1/2002 - 5/31/2007, $300,000.

Courses taught this and last academic year term-by-term

Academic advising: 5

Assigned advisor for 18 undergraduate students during 2004/2005 academic year.

Brief description of major research and scholarly activities:

1. Monte Carlo model checking
One of the major challenges in computer aided verification is state explosion: the phenomenon where the size of a system's state space grows exponentially in the size of its specification. State explosion can render verification intractable for many applications of practical interest. To combat state explosion, we currently work at the development of randomized, Monte Carlo algorithms for static and run-time verification of discrete and continuous reactive systems. These algorithms allow to trade time and space for precision.

2. Compositional Models for Embedded Systems

The distinctive feature of any successful engineering or formal method is scalability, a feature achievable only in a framework supporting on the one hand modular and stepwise system description and on the other hand assume-guarantee and stepwise-refinement reasoning. The aim is to describe and verify synchronous and asynchronous components in a uniform way. The description techniques are based on the modern engineering notations standardized in UML like state transition diagrams, activity diagrams (workflows) and collaboration diagrams that. The verification techniques involve a variety of model-checking algorithms that exploit the hierarchic structure of a component both to improve efficiency and to support abstraction mechanisms and assume guarantee reasoning. They are also well suited in the automated generation of business workflows given a specific problem and a library of tasks. We already have important results on this subject and I hope to demonstrate the utility of these results on problems that could not be addressed by earlier methods.

3. Hybrid Systems

The area of hybrid systems is a very attractive area for research: there seem to be a lot of fundamental mathematical problems that are not yet addressed, and there is a wealth of real applications such as automated highway systems, air-traffic controllers and molecular biology. The continuous dynamics has been well studied in control theory, while automata and concurrency theory are well suited to model the discrete aspects. It is the combination that makes the problems of hybrid systems exciting. There is a growing community of researchers focusing on these problems. However, little work has been done to apply scalable engineering techniques in this area. For example, modular and stepwise description techniques are very promising for efficient simulation and code generation. Compositional reasoning and stepwise refinement promise to improve the current model checking algorithms. A particularly interesting application domain of hybrid systems is modeling the cell behavior. We have already started work in this direction at UPenn and found it extremely exciting.

4. Requirements Analysis

A widespread but rather informal notation for requirements capture both in the telephone industry and in the object oriented methods are interaction diagrams, also known as message sequence charts (MSC). We have developed formal models and notations for MSC both for discrete and hybrid systems and we currently integrate them in Mocha, Hermes and Charon. There are many open research questions related to MSC that we would like to explore such as, modular and stepwise system description, compositional and stepwise-refinement reasoning, application of model checking algorithms and relation to behavior diagrams. Our goal is to help designers detect potential faults at a very early stage. This can also lead to formal links between the groups for requirements specification (beginning of the design cycle) and groups for code-testing (end of the design cycle). Currently we also investigate an alternative formalism that captures shared memory communication.