Advanced Formal Methods for Reliable Critical Systems Software AFOSR F49620-95-1-0508 Progress Report 15 Aug 95 - 31 July 96 Insup Lee Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104-6389 Tel: (215) 898-3532 Fax: (215) 898-0587 Email: lee@cis.upenn.edu Rance Cleaveland, Department of Computer Science, N.C. State University Philip M. Lewis, Department of Computer Science, SUNY at Stony Brook Scott A. Smolka, Department of Computer Science, SUNY at Stony Brook Oleg Sokolsky, Computer Command and Control Company, Philadelphia, PA OBJECTIVES + Development of Design Formalism - Process-Algebra-Based Specification Formalisms for Critical Systems - Executable Specifications - Logics for Specifying Critical Properties of Critical Systems - From Formal Specifications to Executable Code + Design of Analysis Techniques - Automated Techniques for Verifying Critical Systems Software - Advanced Diagnostic Techniques + Tool Implementation - Graphical User Interface - Textual User Interface - Specifications Compiler STATUS OF EFFORT In terms of design formalisms, progress has been made on specification logics, graphical specification languages, and algebraic theories for soft-real time, schedulability, probability, and timing predictability. Regarding analysis techniques, new model-checking algorithms have been developed and implemented for fragments of the modal mu-calculus. Also, a real-time process algebra has been extended with dynamic priorities and was used to perform schedulability analysis of real-time systems with earliest deadline first and priority inheritance protocol. Concerning tool implementation, a redesign of the Concurrency Factory, so that it can better cope with the demands of critical systems analysis, is underway. ACCOMPLISHMENTS/NEW FINDINGS + More efficient algorithms have been developed for determining when finite-state systems enjoy properties expressed in the modal mu-calculus, an expressive specification logic. In principle, these algorithms permit the handling of much larger systems than previous algorithms; implementations and a case study indicate that this is the case in practice as well. These algorithms may be used to check the correctness of finite-state safety-critical system designs, such as those found in flight controllers and guidance systems. + A semantics for soft real-time systems was defined. This theory permits the modeling of probabilistic real-time systems and allows users to make rigorous statements about the likelihood with which systems are guaranteed to meet deadlines. This theory is of fundamental importance for the project, as it will serve as the foundation for the critical-system analysis software we are developing. It also represents an advance over existing models, which typically only support the analysis of hard real-time systems in which no deadlines can ever be missed. + Schedulability analysis has been carried out using a real-time process algebra. To engineer reliable real-time systems, it is desirable to detect timing anomalies early in the development process. However, there is little work addressing the problem of accurately predicting timing properties of real-time systems before implementations are developed. Our research shows that it possible to integrate results from scheduling theory with formal methods. PERSONNEL SUPPORTED * Faculty Rance Cleaveland, N.C. State University Insup Lee, University of Pennsylvania Philip M. Lewis, SUNY at Stony Brook Scott A. Smolka, , SUNY at Stony Brook Oleg Sokolsky, Computer Command and Control Company * Post-Docs Jin-Young Choi, University of Pennsylvania Vijay Gehlot, University of Pennsylvania Xinxin Liu, SUNY Stony Brook Y.S. Ramakrishna, SUNY Stony Brook * Graduate Students Hanene Ben-Abdallah, University of Pennsylvania Hee Hwan Kwak, University of Pennsylvania Zeynep Dayar, North Carolina State University Brad Mott, North Carolina State University PUBLICATIONS * Book Insup Lee and Scott A. Smolka (Eds.), CONCUR~'95: Concurrency Theory, 6th International Conference, Lecture Notes in Computer Science, Volume 962, Springer-Verlag, Berlin (Aug. 1995). * Journals "The Soundness and Completeness of ACSR (Algebra of Communicating Share Resources)," Patrice Bremond-Gregoire, Jin-Young Choi, and Insup Lee, submitted to Information and Computation (Nov 1995). "An Efficient State Space Generation for Analysis of Real-time Systems" by Inhye Kang, Insup Lee and Young Si Kim, submitted to IEEE transactions on Software Engineering (Jan 1996). "An operational framework for synchronous and asynchronous value-passing processes," by Rance Cleaveland and Daniel Yankelevich. Submitted to ACM Transactions on Programming Languages and Systems. "A Process Algebra of Communicating Shared Resources with Dense Time and Priorities," Patrice Bremond-Gregoire and Insup Lee, Theoretical Computer Science, accepted June 1996. "Modeling and verifying distributed systems using priorities: A case study," by Rance Cleaveland, Gerald Luettgen, V. Natarajan and Steven Sims, Software Concepts and Tools, accepted April 1996. "Modeling and verifying active structural control systems," by Wael Elseaidy, Rance Cleaveland and John Baugh, Science of Computer Programming, accepted May 1996. Y.-J. Joung and S.A. Smolka, "A Comprehensive Study of the Complexity of Multiparty Interaction." Journal of the ACM, Vol. 43, No. 1, pp. 75-115 (January 1996). R. van Glabbeek, S.A. Smolka, and B.U. Steffen, "Reactive, Generative, and Stratified Models of Probabilistic Processes." Information and Computation, Vol. 121, No. 1, pp. 59-80 (August 1995). J.C.M. Baeten, J.A. Bergstra, and S.A. Smolka, "Axiomatizing Probabilistic Processes: ACP with Generative Probabilities." Information and Computation, Vol. 121, No. 2, pp. 234-255 (September 1995). S.A. Smolka and B. Steffen, "Priority as Extremal Probability." Formal Aspects of Computing. To Appear (1996). S.-H. Wu, S.A. Smolka, and E. Stark, "Compositionality and Full Abstraction for Probabilistic I/O Automata." Theoretical Computer Science. To Appear (1997). * Conferences "An Efficient State Space Generation for Analysis of Real-time Systems" by Inhye Kang and Insup Lee, International Symposium on Software Testing and Analysis, Jan. 1996. "Schedulability and Safety Analysis in GCS," by Hanene Ben-Abdallah, Young Si Kim and Insup Lee, presented at WORDS 96: Second International Workshop on Object-oriented Real-time Dependable Systems, Feb 1-2, 1996. "Ordering Processes in a Real-Time Process Algebra," by P. Br\'emond-Gr\'egoire, H. Ben-Abdallah and I. Lee, to be presented at Algebraic Methodology and Software Technology Third International Workshop on Real-Time Systems, Salt Lake City, UT, March 1996. "An Automaton Based Algebra For Specifying Robotic Agents," Jana Kovsecka and Hanene Ben-Abdallah, Proc. of 3rd AMAST Workshop on Real-Time Systems, March 1996 "A Theory of Testing for Soft Real-Time Processes," R. Cleaveland, I. Lee, P. Lewis, S.A. Smolka, invited to the Eighth International Conference on Software Engineering and Knowledge Engineering (SEKE'96), June 10-12, 1996. "Testing-Based Analysis of Real-Time System Models," D. Clarke and I. Lee, to appear in Proceedings of International Test Conference, Oct 1996. "XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Systems," D. Clarke, H. Ben-Abdallah, I. Lee, H. Xie and O. Sokolsky, Computer Aided Verification: 8th International Conference, CAV '96, Springer-Verlag LNCS 1102, July/August 1996. "A State Minimization Technique for Timed Automata," Inhye Kang, Insup Lee and Young Si Kim, INFINITY Workshop, Aug 1996. "Efficient local model checking for fragments of the modal mu-calculus," by Girish Bhat and Rance Cleaveland. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 107--126, Passau, Germany, March 1996. Springer-Verlag. "Efficient model checking via the equational mu-calculus," by Girish Bhat and Rance Cleaveland. In Eleventh Annual Symposium on Logic in Computer Science (LICS '96), pages 304--312, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. "Optimality and abstraction in model checking," by Rance Cleaveland, S.P. Iyer and Daniel Yankelevich. In A. Mycroft, editor, Static Analysis, volume 983 of Lecture Notes in Computer Science, pages 51--63, Glasgow, UK, September 1995. Springer-Verlag. "The Concurrency Factory software development environment," by Rance Cleaveland, Philip Lewis, Scott Smolka and Oleg Sokolsky. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 107--126, Passau, Germany, March 1996. Springer-Verlag. "The Concurrency Factory: A development environment for concurrent systems," by Rance Cleaveland, Philip Lewis, Scott Smolka and Oleg Sokolsky. In R. Alur and T. Henzinger, editors, Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 398--401, New Brunswick, NJ, July 1996. Springer-Verlag. "A process algebra with distributed priorities," by Rance Cleaveland, Gerald Luettgen and V. Natarajan. To appear in CONCUR '96, Lecture Notes in Computer Science, Pisa, Italy, August 1996. Springer-Verlag. "Priorities for verifying distributed systems," by Rance Cleaveland, Gerald Luettgen, V. Natarajan and Steven Sims. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 107--126, Passau, Germany, March 1996. Springer-Verlag. "The NCSU Concurrency Workbench," by Rance Cleaveland and Steve Sims. In R. Alur and T. Henzinger, editors, Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 394--397, New Brunswick, NJ, July 1996. Springer-Verlag. "Formal timing analysis for fault-tolerant active structural control systems," by Wael Elseaidy, Rance Cleaveland and John Baugh. In Proceedings of the First Workshop on Formal Methods in System Practice, San Diego, January 1996. "An algebraic theory of process efficiency," by V. Natarajan and Rance Cleaveland. In Eleventh Annual Symposium on Logic in Computer Science (LICS '96), pages 63--72, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. "Predictability of real-time systems: A process-algebraic approach," by V. Natarajan and Rance Cleaveland. To appear in Real-Time Systems Symposium, Washington, DC, December 1996. IEEE Computer Society Press. Y.-J. Joung and S.A. Smolka, "Strong Interaction Fairness via Randomization," 16th IEEE International Conference on Distributed Computing Systems, Hong Kong (May 1996). INTERACTIONS/TRANSITIONS "A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems," Insup Lee, Oxford Workshop on Formal Methods, Oxford, UK, June 1996. ``A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems,'' University of Warwick, UK, June 1996. Workshop on Software Engineering and Programming Languages, Sponsored by ARO and NSF, June 12-13, Boston. "ACSR-VP: A Timed Process Algebra for the Specification and Analysis of Real-Time Systems," Insup Lee, ARO Workshop, Raleigh, Feb 1996. "The Specification and Schedulability Analysis of Real-Time Systems using ACSR," Insup Lee, AT&T SUNY-SB Workshop on Specification and Verification, SUNY-Stony Brook, Nov 1995. "The Concurrency Factory Software Development Environment," Rance Cleaveland, Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, Mar 1996. "Mu-Calculus Model Checking via LTL Model Checking," Rance Cleaveland, AT&T SUNY-SB Workshop on Specification and Verification, SUNY-Stony Brook, Nov 1995. "Verifying Fault-Tolerant Active Structural Control Systems," Rance Cleaveland, AT&T Bell Laboratories Seminar, Oct 1995. "PARAGON Toolset," Oleg Sokolsky, CAV'96, New Brunswick, NJ, July 1996 Presentation by S.A. Smolka on "Semantic Theories and Automated Tools for Real-Time and Probabilistic Concurrent Systems," ARPA Formal Methods PI Meeting, San Diego, CA, January 1996. Presentation by S.A. Smolka on "Fighting Livelock in the i-Protocol with the Concurrency Factory," Workshop on Academic Electronics, Rome Laboratories, Syracuse, NY, June 1996. Presentation by S.A. Smolka on "Automated Formal Verification in the Concurrency Factory," Workshop on Automated Formal Methods, Oxford University, Oxford, England, June 1996. Presentation by S.A. Smolka on "A Complete Axiom System for Finite-State Probabilistic Processes," Universidad Complutense Madrid, Spain, June 1996. Presentation by S.A. Smolka on "A Weak-Modality-Based Partial-Order Reduction Technique," Workshop on Concurrency Theory and Applications, Kyoto University, Japan, July 1996. * Consultative And Advisory Functions To Other Laboratories And Agencies Rance Cleaveland served on a review panel for the NSF/DARPA Evolutional Development of Complex Systems Initiative, Apr 1996 (Helen Gill was NSF contact, John Salasin was DARPA contact). Scott Smolka served on an NSF SBIR Phase II review panel, January 1996. * Transitions Rance Cleaveland, Gilbarco Corporation, tutorial on finite-state machines and software development. Enabling research: mechanisms for describing concurrent and interacting finite-state machines. Contact: Bill Royal. The formal methods developed through the current research are utilized by Computer Command and Control Company (CCCC). The company uses the advances in graphical specification languages and real-time verification techniques, in an effort to build an industry-strength specification and analysis environment for real-time systems. Specifically, the environment is built around GCSR specification language developed by the Real-Time Systems group (RTG) in the University of Pennsylvania. Intuitive primitives of the language allow efficient specifications, while operational semantics of GCSR enable interactive simulation of the specifications. Analysis capabilities are based on efficient state-space exploration techniques developed by the RTG. The person in CCCC responsible for the application of formal methods is Dr. Oleg Sokolsky (sokolsky@cccc.com). New DISCOVERIES, INVENTIONS, OR PATENT DISCLOSURES none HONORS/AWARDS none