Servicenavigation

Project Details

Back

Projekt Print View

Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic

Applicant Professor Dr. Gerald Lüttgen, since 5/2020
Subject Area Theoretical Computer Science
Term from 2013 to 2024
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 233929853
 
Final Report Year 2024

Final Report Abstract

Reactive systems continuously sense parameters of their physical environment and compute reactions that drive actuators influencing the environment. The component-based software of such systems implements, in essence, concurrent state machines, and is often specified abstractly via propositional and temporal logics. Hence, reactive system design can profit from heterogenous languages that mix logical and operational paradigms. It also calls for a notion of behavioural refinement for compositionally reasoning about the behaviour of concurrently interacting components, which must be sensitive to communication error and deadlock. The research project’s starting point were interface theories based on de Alfaro and Henzinger’s interface automata (IA) and specification theories based on Larsen’s modal transition systems (MTS). These formalisms are all based on state machines, support concurrency, allow abstract modelling via nondeterminism, and permit stepwise refinement via a behavioural preorder. To achieve this, the formalisms impose grave restrictions regarding nondeterminism, compositional reasoning and abstraction from internal computation, and lack support of the logic specification paradigm. The present project set out to remove these shortcomings and significantly enhance the theoretical foundations and practical utility of heterogenous specification formalisms. We achieved this goal by, firstly, studying the subtle interplay between communication error, nondeterminism and compositionality. A communication error arises when an output event of one component is not expected by another. We then developed the new interface theory MIA (Modal Interface Automata) which permits nondeterminism wrt. output and input events. MIA adapts the MTS modal refinement in a truly compositional way, respects communication errors, and properly abstracts from internal computation. Secondly, we embedded the temporal logic ACTL into MIA so that model checking becomes refinement and can be performed compositionally. Conjunction allows for a component to satisfy multiple interfaces by refining the interfaces’ conjunction. Thirdly, we put our foundational work into practice by exploring the extent to which shared variable communication can be added to interface theories, where variable manipulations are expressed via pre-/post-conditions. For the resulting IAM formalism (Interface Automata with shared Memory) and also for MIA, we built a toolset consisting of an editor, a simulator and a refinement checker. Last, but not least, we applied our knowledge to DLR’s Virtual Satellite (VirSat) language, which is used in the model-driven development of spacecraft software and employs logic constraints for synchronizing state machines. We developed a formal semantics for VirSat and supported the envisaged refinement-based methodology by a compositional refinement preorder.

Publications

 
 

Additional Information

© 2025 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung