6 citations · 7 across the 7 of their papers we have counts for
7 papers
The Refinement Calculus of Reactive Systems Toolset
Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis
We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional modeling and reasoning about reactive systems, built on top of Isabelle, Simulink,…
The Refinement Calculus of Reactive Systems
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to d…
Type Inference of Simulink Hierarchical Block Diagrams in Isabelle
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
Simulink is a de-facto industrial standard for the design of embedded systems. In previous work, we developed a compositional analysis framework for Simulink models in Isabelle --…
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics,…
Translating Hierarchical Block Diagrams into Composite Predicate Transformers
Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis
Simulink is the de facto industrial standard for designing embedded control systems. When dealing with the formal verification of Simulink models, we face the problem of translatin…
Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
Viorel Preoteasa, Stavros Tripakis
Feedback is an essential composition operator in many classes of reactive and other systems. This paper studies feedback in the context of compositional theories with refinement. S…