research-article

Co-simulating event-B and continuous models via FMI

Authors:

Vitaly Savicks,

Michael Butler,

John ColleyAuthors Info & Claims

SummerSim '14: Proceedings of the 2014 Summer Simulation Multiconference

Article No.: 37, Pages 1 - 8

Published: 06 July 2014 Publication History

Abstract

We present a generic co-simulation approach between discrete-event models, developed in the Event-B formal method, and continuous models, exported via the Functional Mock-up Interface for Co-simulation standard. The concept is implemented into a simulation extension for the Rodin platform, thus leveraging powerful capabilities of refinement-based modelling and deductive verification in Event-B while introducing a continuous-time aspect and simulation-based validation for the development of complex hybrid systems.

References

[1]

Edward A. Lee. Cyber physical systems: Design challenges. In International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), May 2008. Invited Paper.

Digital Library

[2]

K. Balasubramanian, A. Gokhale, G. Karsai, J. Sztipanovits, and S. Neema. Developing applications using model-driven design environments. Computer, 39(2):33--40, 2006.

Digital Library

[3]

Torsten Blochwitz, M Otter, M Arnold, C Bausch, C Clauß, H Elmqvist, A Junghanns, J Mauss, M Monteiro, T Neidhold, et al. The Functional Mockup Interface for tool independent exchange of simulation models. In Modelica'2011 Conference, March, pages 20--22, 2011.

[4]

Stefania Gnesi and Tiziana Margaria. Formal Methods for Industrial Critical Systems. Wiley Online Library, 2013.

[5]

S. Liu and R. Adams. Limitations of formal methods and an approach to improvement. In Software Engineering Conference, 1995. Proceedings., 1995 Asia Pacific, pages 498--507. IEEE, 1995.

Digital Library

[6]

A. Hall. Seven myths of formal methods. Software, IEEE, 7(5):11--19, 1990.

Digital Library

[7]

J. R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer (STTT), 12(6):447--466, 2010.

Digital Library

[8]

Jean-Raymond Abrial and Stefan Hallerstede. Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, 77(1):1--28, 2007.

Digital Library

[9]

Michael Jastram. ProR, an open source platform for requirements engineering based on RIF. 2010.

[10]

C. Snook and M. Butler. UML-B and Event-B: an integration of languages and tools. 2008.

[11]

Michael Leuschel and Michael Butler. ProB: an automated analysis toolset for the B method. International Journal on Software Tools for Technology Transfer, 10(2):185--203, 2008.

Digital Library

[12]

Steve Wright. Automatic generation of C from Event-B. In Workshop on integration of model-based formal methods and tools. Citeseer, 2009.

[13]

Andrew Edmunds and Michael Butler. Tasking Event-B: An extension to Event-B for generating concurrent code. 2011.

[14]

Jean-Raymond Abrial Wen Su and Huibiao Zhu. Complementary methodologies for developing hybrid systems with Event-B, 2012.

[15]

Jean-Raymond Abrial, Wen Su, and Huibiao Zhu. Formalizing hybrid systems with Event-B. In Abstract State Machines, Alloy, B, VDM, and Z, pages 178--193. Springer, 2012.

Digital Library

[16]

Richard Banach and Michael Butler. A hybrid Event-B study of lane centering. In Complex Systems Design & Management, pages 97--111. Springer, 2014.

[17]

MODELISAR. Functional Mock-up Interface for Co-Simulation, Version 1.0. https://svn.modelica.org/fmi/branches/public/specifications/FMI_for_CoSimulation_v1.0.pdf, October 2010.

[18]

S. Tudoret, S. Nadjm-Tehrani, A. Benveniste, and J. E. Strömberg. Co-simulation of hybrid systems: Signal-Simulink. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 623--639. Springer, 2000.

Digital Library

[19]

J. Fitzgerald, P. Larsen, K. Pierce, M. Verhoef, and S. Wolff. Collaborative modelling and co-simulation in the development of dependable embedded systems. In Integrated Formal Methods, pages 12--26. Springer, 2010.

Digital Library

[20]

Christopher Brooks, Edward A Lee, Xiaojun Liu, Yang Zhao, Haiyang Zheng, Shuvra S Bhattacharyya, Elaine Cheong, Mudit Goel, Bart Kienhuis, Jie Liu, et al. Ptolemy II: Heterogeneous concurrent modeling and design in Java. 2005.

[21]

Ralph-JR Back. Refinement calculus, part II: Parallel and reactive programs. In Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness, pages 67--93. Springer, 1990.

[22]

J. Abrial, M. Lee, D. Neilson, P. Scharbach, and I. Sørensen. The B-method. In VDM'91 Formal Software Development Methods, pages 398--405. Springer, 1991.

Digital Library

[23]

Torsten Blochwitz, Martin Otter, Johan Akesson, Martin Arnold, Christoph Clauss, Hilding Elmqvist, Markus Friedrich, Andreas Junghanns, Jakob Mauss, Dietmar Neumerkel, et al. Functional mockup interface 2.0: The standard for tool independent exchange of simulation models. In 9th International Modelica Conference, Munich, 2012.

[24]

R Kübler and W Schiehlen. Two methods of simulator coupling. Mathematical and Computer Modelling of Dynamical Systems, 6(2):93--113, 2000.

[25]

Jens Bastian, Christoph Clauß, Susann Wolf, and Peter Schneider. Master for co-simulation using FMI. In 8th International Modelica Conference. Dresden, 2011.

[26]

Tom Schierz, Martin Arnold, and Christoph Clauß. Co-simulation with communication step size control in an FMI compatible master algorithm. In 9th International Modelica Conference. Munich, 2012.

[27]

David Harel. Statecharts: A visual formalism for complex systems. Science of computer programming, 8(3):231--274, 1987.

Digital Library

[28]

Edwin Seidewitz. What models mean. Software, IEEE, 20(5):26--32, 2003.

Digital Library

[29]

Birron Mathew Weedy, Brian John Cory, N Jenkins, JB Ekanayake, and G Strbac. Electric power systems. John Wiley & Sons, 2012.

[30]

Modelica Association et al. Modelica -- a unified object-oriented language for physical systems modeling. Language Specification, Version, 2, 2005.

[31]

Mohammad Moradzadeh and René Boel. A hybrid framework for coordinated voltage control of power systems. In IPEC, 2010 Conference Proceedings, pages 304--309. IEEE, 2010.

Cited By

Liboni GDeantoni JPortaluri AQuaglia Dde Simone RChillet D(2018)Beyond Time-Triggered Co-simulation of Cyber-Physical Systems for Performance and Accuracy ImprovementsProceedings of the Rapido'18 Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools10.1145/3180665.3180668(1-8)Online publication date: 22-Jan-2018
https://dl.acm.org/doi/10.1145/3180665.3180668
(2017)Stepwise construction of a metabolic network in Event-BComputers in Biology and Medicine10.1016/j.compbiomed.2017.09.02191:C(1-12)Online publication date: 1-Dec-2017
https://dl.acm.org/doi/10.1016/j.compbiomed.2017.09.021
Hoang TSnook CLadenberger LButler M(2016)Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-SimulationProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_31(360-375)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_31
Show More Cited By

Recommendations

Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
Building traceable Event-B models from requirements

Bridging the gap between informal requirements and formal specifications is a key challenge in systems engineering. Constructing appropriate abstractions in formal models requires skill and managing the complexity of the relationships between ...
Proving the Fidelity of Simulations of Event-B Models
HASE '14: Proceedings of the 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering

A major hindrance to the use of formal methods is the difficulty to validate the models, particularly at the early stages of the development. We propose to build simulations: programs automatically generated from the specifications but with user-...

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

SummerSim '14: Proceedings of the 2014 Summer Simulation Multiconference

July 2014

539 pages

Sponsors

SCS: Society for Modeling and Simulation International

In-Cooperation

SIGSIM: ACM Special Interest Group on Simulation and Modeling

Publisher

Society for Computer Simulation International

San Diego, CA, United States

Publication History

Published: 06 July 2014

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SummerSim '14

Sponsor:

SCS

SummerSim '14: 2014 Summer Simulation Multiconference

July 6 - 10, 2014

California, Monterey

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
95
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liboni GDeantoni JPortaluri AQuaglia Dde Simone RChillet D(2018)Beyond Time-Triggered Co-simulation of Cyber-Physical Systems for Performance and Accuracy ImprovementsProceedings of the Rapido'18 Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools10.1145/3180665.3180668(1-8)Online publication date: 22-Jan-2018
https://dl.acm.org/doi/10.1145/3180665.3180668
(2017)Stepwise construction of a metabolic network in Event-BComputers in Biology and Medicine10.1016/j.compbiomed.2017.09.02191:C(1-12)Online publication date: 1-Dec-2017
https://dl.acm.org/doi/10.1016/j.compbiomed.2017.09.021
Hoang TSnook CLadenberger LButler M(2016)Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-SimulationProceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 967510.1007/978-3-319-33600-8_31(360-375)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1007/978-3-319-33600-8_31
Lee ENiknami MNouidui TWetter MGirault AGuan N(2015)Modeling and simulating cyber-physical systems using CyPhySimProceedings of the 12th International Conference on Embedded Software10.5555/2830865.2830878(115-124)Online publication date: 4-Oct-2015
https://dl.acm.org/doi/10.5555/2830865.2830878
Brooks CLee ELorenzetti DNouidui TWetter MGirard ASankaranarayanan S(2015)CyPhySimProceedings of the 18th International Conference on Hybrid Systems: Computation and Control10.1145/2728606.2728641(301-302)Online publication date: 14-Apr-2015
https://dl.acm.org/doi/10.1145/2728606.2728641

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents