9734115 Model checking is emerging as a practical tool for automated debugging of complex reactive systems. In model checking, a high- level description of a system is compared against a logical correctness requirement to discover inconsistencies. This CAREER research aims to enhance applicability and efficiency of this paradigm by pursuing three objectives in research and education. First, to make results in computer-aided verification more accessible to nonspecialists, a modeling method called "reactive modules" is developed as a unified framework. In addition, an analysis tool that supports a combination of techniques, a standard textbook on computer-aided verification, and an advanced course on computer-aided verification will all be created. Second, to develop techniques that can analyze systems beyond the reach of existing tools, two new topics, open systems and heterogeneous systems, are investigated. An open system is a reactive system interacting with an unspecified environment, and for analysis of such systems, novel specification paradigms such as alternating-time temporal logics are studied. For analysis of systems consisting of components with different synchrony assumptions and described in different source languages, the utility of reactive modules as a common semantic framework is investigated. Finally, to integrate concepts in formal methods into undergraduate education at Penn, changes to existing courses in theory and systems are proposed.***
