Amir Pnueli

Statemate was designed and built between 1984 and 1986 by a team composed of David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Mark Trakhtenbrot, and Aron Trauring at Ad Cad, Ltd., which later became the R&D division of I-Logix, Inc. It has been available continuously since then in several increasingly sophisticated versions.

Statemate had a fundamental impact on software and systems engineering. The ideas first appearing in Statemate underlie today's most powerful and most widely used tools in software and systems engineering. Before Statemate, graphical design notations supported by CASE (computer-aided software engineering) tools did not have formal foundations, could not execute models, and could not generate code that ran. They were like programming language environments without compilers and interpreters.

In 1983, David Harel developed statecharts, a graphical language for finite-state machines. The language provided natural and easy-to-grasp abstraction features, such as hierarchy, parallelism, and aggregation, which facilitate human understanding of complex system behavior. Harel and Pnueli then identified the class of reactive systems, for which such behavioral aspects were most problematic. Reactive systems include concurrent and real-time systems, embedded systems, and interactive systems. Statecharts proved to be the right notation to model them.

In early 1984, Harel, Lachover, and Pnueli, together with Ido Lachover, co-founded Ad Cad, Ltd., to build a CASE tool supporting statecharts. One of the group's first tasks was to figure out how to embed statecharts into a broader framework that would capture the structure and functionality of a large complex system. They devised two more diagrammatic languages: activity charts, to specify functionality, and module charts, to specify structure.

The first version of Statemate was operational in 1986. A Statemate user could draw a model's artifacts, check and analyze them, produce documentation, and manage their configurations and versions. Most importantly, Statemate could execute the model's functional and behavioral descriptions and could automatically generate executable code.

Statemate was the first real-world tool for model-driven system development (MDD). In the 1990s, statecharts were incorporated into the Unified Modeling Language (UML), the industry-standard language for specifying, visualizing, constructing, and documenting the artifacts of software systems, and the basis for many recent CASE tools.

Amir Pnueli made a major breakthrough in the verification and certification of concurrent and reactive systems with his landmark 1977 paper "The Temporal Logic of Programs"(1) which was a crucial turning point in the progress of formal methods for such systems. This paper triggered a fundamental paradigm shift in reasoning about the dynamic behavior of systems; the techniques it introduces have had extraordinary influence and proven to be of lasting value. His work has been characterized as the most important contribution to program verification in the last twenty years and it has set the agenda for research and practice in the area.

Pnueli's work on temporal logic has been seminal. First, he focused on the ongoing behavior of programs rather than just their input/output behavior thereby introducing a powerful formalism for reasoning about programs. Second, by using temporal logic he made it possible to easily specify qualitative progress properties of concurrent programs without cumbersome timing details. Third, he recognized the value of carefully-chosen dedicated operators to deal with the temporal ordering of events and thereby establish a framework for reasoning about and mechanical verification of concurrent programs.

Beyond his pure scientific achievements, Amir Pnueli, a Professor of Computer Science at the Weizmann Institute of Science in Israel, is also keenly aware of the problems of putting computer science methods into practice and has been instrumental in founding two Israeli software firms. His work has influenced a large number of diverse industrial applications such as the process control of chemical plants, rule languages in active database systems, and the detection of complex race conditions in cache coherence protocols of computer architectures. By introducing temporal logic to computer science, Amir Pnueli has made a significant and lasting contribution which has been instrumental in shaping the study of concurrent systems.

(1) Proc. 18th IEEE Symp. Found. of Comp. Sci., 1977, pp. 46-57