Objectives

To develop a formal framework for designing and analyzing critical systems. We will also implement an advanced CASE environment that uses this framework in providing tools for overseeing the modular design and implementation of such systems. There are three main tasks.

1. Development of Design Formalism
2. Design of Analysis Techniques
3. Tool Implementation

Approach

The approach toward above object is based on process algebra, a formal framework for the specification and verification of systems of interacting concurrent and distributed processes. Our research will focus on scaling up process algebra to handle the myriad complexities of critical systems software. For achieving this goal, we will develop toolsets and CASE environment for the specification, simulation, automated analysis, and implementation of reliable critical systems software.

Researchers

Faculty

• Rance Cleaveland - North Carolina State University, rance@csc.ncsu.edu
• Insup Lee - University of Pennsylvania, lee@cis.upenn.edu
• Philip M.Lewis - SUNY at Stony Brook, pml@sbcs.sunysb.edu
• Scott A.Smolka - SUNY at Stony Brook, sas@cs.sunysb.edu

Postdoc

• Xinxin Liu - SUNY Stony Brook
• Anna Philippou - University of Pennsylvania
• Y. S. Ramakrishna - SUNY at Stony Brook, ysr@cs.sunysb.edu

Industrial Partners

• Oleg Sokolsky - CCCC, sokolsky@banana.cccc.com

Graduate Students

• Zeynep Dayar - North Carolina State University, zdayar@unity.ncsu.edu
• Yifei Dong - SUNY at Stony Brook, ydong@cs.sunysb.edu
• Vic Du - SUNY at Stony Brook, vicdu@cs.sunysb.edu
• Hee Hwan Kwak - University of Pennsylvania, heekwak@saul.cis.upenn.edu
• Bradford W. Mott - North Carolina State University, bwmott@eos.ncsu.edu
• Pranav K. Tiwari - North Carolina State University, pktiwari@eos.ncsu.edu
• Mahesh Viswanathan - University of Pennsylvania, maheshv@saul.cis.upenn.edu

Related Projects

• PARAGON/VERSA
• Concurrency Workbench
• Concurrency Factory

Technology Transition

One important aspect of this project is industry participation.

• We can determine the feasibility and scalability of our technique
• They can increase their application's reliability by formal verification

Annual Reports

• 1995-1996
• 1996-1997

Related Links

• Formal Methods
• IEEE-CS Technical Committe on Real-Time Systems
• IEEE-CS Technical Council on Software Engineering

If you have any questions or comments about this page, please drop me a line. leahhc@saul.cis.upenn.edu

You are thevisitor.

Last update: October 20, 1997