Logotype Mälardalenn University
This web site has been moved.
Please visit our new and improved web site at: http://www.es.mdh.se/
Startpage www.mdh.se

The Formal Modeling of Timing and Resources Research Direction

Researchers involved

Paul Pettersson (Professor), Cristina Seceleanu (Senior Lecturer), Kang Eun Young (PostDoc), Aneta Vulgarakis (PhD Student), Jagadish Suryadevara (PhD Student), Marin Orlic (PhD Student).

Context and research overview

The Formal Modelling of Timing and Resources Research Direction has focused on behaviour models and on providing support for model-based analysis of the PROGRESS component architectural and analysis models. In particular, the contributed behavioural model REMES allows for modelling of functional, timing and resource-wise behaviour of components. The language has a formally defined syntax and semantics. To allow for analysis of combined ProCom and REMES models, we have provided a formal semantics of the PROGRESS architectural component models. The semantics are given by transformation to (priced) timed automata, which allows to transform combined models to the model-checking tool UPPAAL for simulation and property verification. We have also developed automated tool support, which is integrated in the PROGRESS IDE.

Major results

Highlight 8 - REMES - a REsource Model for Embedded Systems [Show]

REMES is a resource model for modelling functional, timing, and resource-wise behaviour of ProCom-based systems [29, 30]. To support model-based development with REMES models, we have developed the REMES meta model and a REMES editor, in which valid REMES behavioural models can be constructed. Further, to support analysis of REMES models, we have defined analysis goals for REMES models in WCTL, that is, we have formalized feasibility analysis, optimal resource-usage and trade-off analysis goals for ProCom-based systems.

Highlight 9 - Formal semantics of ProCom [Show]

We have developed a formal semantics of ProSys and ProSave components in terms of finite state machines extended with urgency and priorities on transitions [31]. The scientific challenge has been to develop the semantics, but also to give the semantics in such a way that it is useful for engineers using the model, and developing tool support based on the semantics. The result has proven useful as a base for developing tool support for the model and its combination with REMES.

Highlight 10 - Bridging semantic gaps between PROGRESS models [Show]

We have proposed patterns for bridging the semantic gap between specification models (given as mode automata) and ProCom-based architectural models [32, 33, 34]. This work aims to develop support for relating high-level specification and requirement models to design models for ProCom. We have developed a rigorous framework, based on inference rules and simulation relations, for proving that ProCom-based design models (time-triggered, pipes and filters), are meeting the specification models (event based, implicit time, timeouts).

Highlight 11 - Tool development [Show]

We have defined and automated the REMES to PTA transformation [29]. We have implemented a REMES simulator, in which behavioural models can be "run" in order to depict initial trouble spots before proceeding to full formal analysis [35]. We have integrated the REMES editor, REMES to PTA transformation, and verification engine (UPPAAL CORA) into PrIDE. We have defined and implemented the connection between ProCom and REMES. Another tool result is the UPPAAL Port tool [36], which extends the UPPAAL tool with a real-time component model, based on the PROGRESS component model, and a partial order reduction technique utilizing the architectural structure to improve the model-checking efficiency. The tool is available on the web page www.uppaal.org/port. Other tool development includes a simulator and verifier for AADL [37, 38] and a model-to-model transformational approach from EAST-ADL2 to UPPAAL-Port [39].

Highlight 12 - Validation in case studies [Show]

We have worked on validating PROGRESS results in several case studies. In [40], we have validated the full formal modelling and analysis chain or REMES and PROGRESS on a telecom case study in collaboration with Ericsson Nikola Tesla. The work performed partially on-site in collaboration with Ericsson engineers. In [32], we apply PROGRESS component model and analysis techniques to the PROGRESS autonomous truck system. In [41] we apply PROGRESS model and analysis techniques to a turntable system.

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2013.02.25