The European Community Esprit project "Sacres" (Safety Critical Systems: From Specification to Implementation) proposes an integrated approach to the development of software for safety-critical systems, based on a system specification language combining Statecharts with the Synchronous data-flow language Sildex, formal verification of the specification and design, and automatic code-generation from the specification into safety-critical variants of C and Ada.

In this talk, we present the approach of the Sacres project to ensuring the correctness of the code-generator tool (translator). Rather than verifying the translator once and for all, we construct a "validator tool" which verifies each translation as it is produced. The validator accepts as inputs the source and the target code, as it was produced by the translator, and attempts to verify formally that the produced target code is a correct implementation of the source. In case of success, the validator produces a very detailed proof of correctness which can be confirmed by a trivial proof checker. In case of failure, it produces a counter example, indicating a possible mismatch between the source and the target.

We start with a short introduction to synchronous specification languages and their natural "event-based" semantics, and explain some of the difficulties in mapping such a language into typically "state-based" languages such as C. We introduce the main formal tool to be used, which is that of refinement and identify the constructs one has to provide in a refinement proof: A refinement mapping, and an appropriate auxiliary invariant. We show that, while in general, finding these constructs is an undecidable problem, for the case of translation validation this problem can be solved algorithmically. We illustrate the ideas on a simple example and provide details about its automatic verification.

SPEAKER BIO
Amir Pnueli finished his B.Sc. degree in Mathematics at the Technion, Haifa, and received his Ph.D. degree in Applied Mathematics at the Weizmann Institute of Science, Rehovot, Israel, submitting a thesis on "Calculation of Tides in the Ocean" in 1967.

He switched into Computer Science while being a post-doctoral fellow at Stanford University, and at Watson Research Center, Yorktown. He then returned to Israel to a position of a Senior Researcher in the Department of Applied Mathematics of the Weizmann Institute.

In 1973, Prof. Pnueli moved to Tel-Aviv University, where he founded the Department of Computer Science and was its first chairman. In 1981, he returned to the Weizmann Institute, as a Professor of Computer Science.

Prof. Pnueli is the 1996 recipient of the ACM Turing award "For his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification."

Prof. Pnueli is mainly known for the introduction of temporal logic into Computer Science; his work on the application of temporal logic and similar formalisms for the specification and verification of reactive systems; the identification of the class of "Reactive Systems" as systems whose formal specification, analysis, and verification require a distinctive approach; and the development of a rich and detailed methodology, based on temporal logic, for the formal treatment of reactive system; extending this methodology into the realm of real-time systems; and more recently, introducing into formal analysis the models of hybrid systems with appropriate extension of the temporal-logic based methodology.

Beside his more theoretical work, concerning a complete axiom system and proof theory for program verification by temporal logic, he also contributed to algorithmic research in this area.

Amir Pnueli is a member of the steering committees of the conferences CAV (Computer Aided Verification), FTRTFT (Formal Techniques for Real-Time and Fault-Tolerant Systems), and ICTL (International Conference on Temporal Logic).

He is an editor of "Science of Computer Programming", the "Journal of Logic and Computations", "Formal Methods in System Design", and IGPL (Journal of the Interest Group in Pure and Applied Logics). He is a member of the Beirat for the Leibniz Center for Research in Computer Science at the Hebrew University, since its inception in 1985. Pnueli is a member of the IFIP's WG2.2 working group on Formal Description of Programming. He has been on the program committees of POPL, FOCS, LICS, CAV, FTRTFT, Concur, PODC, and ICALP.

In 1971, Prof. Pnueli co-founded the software company Mini-Systems, which until 1982 was the sole software provider for Scitex, Israel, manufacturers of computer aided design systems in the color press and graphic printing areas. During this period, Pnueli designed and supervised several real time mini-computer systems, including message switching, Computer-Aided Teaching, on-line instrument testing, military real time systems, operating systems and compilers.

In 1984, Mini-Systems was acquired by Scitex, and Prof. Pnueli moved on to found, together with two of his previous partners and Prof. David Harel, also from the Weizmann Institute, the company AdCad. In the years 1984-1989, Prof. Pnueli supervised and designed (together with David Harel) the first version of the Statemate system. This implementation effort required continuous research to clarify the semantics of synchronous languages, among which, Statecharts occupy a prominent position.

The company AdCad later evolved into i-Logix, a firm constructing Computer Aided Software Engineering tools for the specification and design of real time reactive embedded systems, and which is the current producer of the various versions of the Statemate systems and its later derivatives.

SCS Distinguished Lecture Schedule
SCS Calendar of Events