Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations
Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets – design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder’s viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive models whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.
Thu 24 Sep Times are displayed in time zone: (UTC) Coordinated Universal Time
08:00 - 09:00: Model-Driven Development and Rapid PrototypingResearch Papers / Tool Demonstrations at Wombat Chair(s): Timo KehrerHumboldt-Universtität zu Berlin | |||
| 08:00 - 08:20 Talk | Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations Research Papers Christos TsigkanosTU Vienna, NIANYU LIPeking University, China, Zhi JinPeking University, Zhenjiang HuPeking University, China, Carlo GhezziPolitecnico di Milano | ||
| 08:20 - 08:40 Talk | Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach Research Papers Chaima BoufaiedUniversity of Luxembourg, Claudio MenghiUniversity of Luxembourg, Luxembourg, Domenico BianculliUniversity of Luxembourg, Lionel BriandSnT Centre/University of Luxembourg, Yago Isasi ParacheLuxSpace | ||
| 08:40 - 08:50 Talk | GUI2WiRe: Rapid Wireframing with a Mined and Large-Scale GUI Repository using Natural Language Requirements Tool Demonstrations Kristian KolthoffInstitute for Enterprise Systems (InES), University Of Mannheim, Christian BarteltInstitute for Software and Systems Engineering, TU Clausthal, Simone Paolo PonzettoData and Web Science Group, University of Mannheim | ||
