Article | Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015 | Formal Requirements Modeling for Simulation-Based Verification
Göm menyn

Title:
Formal Requirements Modeling for Simulation-Based Verification
Author:
Martin Otter: Institute of System Dynamics and Control, DLR, Germany Nguyen Thuy: EDF, France Daniel Bouskela: EDF, France Lena Buffoni: PELAB, Linköping University, Sweden Hilding Elmqvist: Dassault Systèmes AB, Sweden Peter Fritzson: PELAB, Linköping University, Sweden Alfredo Garro: DIMES, University of Calabria, Italy Audrey Jardin: EDF, France Hans Olsson: Dassault Systèmes AB, Sweden Maxime Payelleville: Dassault Aviation, France Wladimir Schamai: Airbus Group Innovations, Germany Eric Thomas: Dassault Aviation, France Andrea Tundis: DIMES, University of Calabria, Italy
DOI:
10.3384/ecp15118625
Download:
Full text (pdf)
Year:
2015
Conference:
Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015
Issue:
118
Article no.:
067
Pages:
625-635
No. of pages:
11
Publication type:
Abstract and Fulltext
Published:
2015-09-18
ISBN:
978-91-7685-955-1
Series:
Linköping Electronic Conference Proceedings
ISSN (print):
1650-3686
ISSN (online):
1650-3740
Publisher:
Linköping University Electronic Press, Linköpings universitet


Export in BibTex, RIS or text

This paper describes a proposal on how to model formal requirements in Modelica for simulation-based verification. The approach is implemented in the open source Modelica_Requirements library. It requires extensions to the Modelica language, that have been prototypically implemented in the Dymola and OpenModelica software. The design of the library is based on the FOrmal Requirement Modeling Language (FORM-L) defined by EDF, and on industrial use cases from EDF and Dassault Aviation. It uses 2- and 3-valued temporal logic to describe requirements.

Keywords: Requirements; verification; physical systems; FORM-L; 3-valued logic; temporal logic; assessment

Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015

Author:
Martin Otter, Nguyen Thuy, Daniel Bouskela, Lena Buffoni, Hilding Elmqvist, Peter Fritzson, Alfredo Garro, Audrey Jardin, Hans Olsson, Maxime Payelleville, Wladimir Schamai, Eric Thomas, Andrea Tundis
Title:
Formal Requirements Modeling for Simulation-Based Verification
DOI:
http://dx.doi.org/10.3384/ecp15118625
References:

C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press. ISBN 978-0-262-02649-9, 2008.


D. Bochvar Ob odnom trekhznachnom ischislenii i ego primenenii k analizu paradoksov klassicheskogo rasshirennogo funkciona’nogo ischislenija. In Matematicheskij Sbornik 4, no 46, pp. 287–308. 1937.


D. Bouskela, N. Thuy, and A. Jardin . D2.1.1 – Modelica extensions for properties modelling, Part II: Modeling Architecture for the Design Verification against System Requirements. Internal report, ITEA2 MODRIO project, March 2015.


M.A. Breuer. A Note on Three-Valued Logic Simulation. IEEE Transaction on Computer C-21, no. 4, pp. 399-402, 1972.


L. Buffoni and P. Fritzson. Expressing Requirements in Modelica. Proceedings of the 55th International Conference on Simulation and Modeling (SIMS 2014), October 21-22, Aalborg, Denmark, 2014.


Dassault Systèmes. Dymola 2016., 2015. http://www.Dymola.com


Department of Defense Aircraf.t Electric Power Characteristics (MIL-STD-704F). 1984. Download: http://everyspec.com/MIL-STD/MIL-STD-0700-
0799/MIL-STD-704F_1083/


A. Garro, A. Tundis, and M. Otter. D2.1.1 – Modelica extensions for properties modelling, Part IVb: FORM-L and Modelica: syntax and relationships. Internal report, ITEA2 MODRIO project, Sept. 2014.


H. Elmqvist, H. Olsson, and M. Otter. Constructs for Meta Properties Modeling in Modelica. Accepted for Modelica’2015 conference, 2015.


A. Jardin and D. Bouskela. D2.1.1 – Modelica extensions for properties modelling, Part I: Users motivation. Internal report, ITEA2 MODRIO project, Sept. 2014.


A. Jardin, D. Bouskel, N. Thuy, N. Ruel, E. Thomas, L. Chastanet, R. Schoenig, and S. Loembé. Modelling of System Properties in a Modelica Framework. Proceedings 8th Modelica Conference, Dresden, Germany, March 20-22., pp. 579-592, 2011. Download: http://www.ep.liu.se/ecp/063/065/ecp11063065.pdf


H. D. Joos. Worst-case parameter search based clearance using parallel nonlinear programming methods. In: Optimization based Clearance of Flight Control Laws. Lecture notes in control and information sciences, 416. Springer, pp. 149-159, 2011. ISBN 978-3-642-22626-7. ISSN 0170-8643.


A. Junghanns, J. Mauss, and M. Tatar. TestWeaver – A Tool for Simulation-based Test of Mechatronic Designs. Proceedings of the Modelica’2008 Confererence, pp. 341-348, March 3-4, 2008. Download: https://www.modelica.org/events/modelica2008/Proceedings/sessions/session3c4.pdf


M. Kuhn, M. Otter and T. Giese. Model Based Specifications in Aircraft Systems Design. Accepted for Modelica’2015 conference, Sept. 2015.


L. Lamport. Principles and Specifications of Concurrent Systems, 2015. Hyberbook: http://research.microsoft.com/enus/um/people/lamport/tla/hyperbook.html


M. Leucker, and C. Schallhart, C. A Brief Account of Runtime Verification. Journal of Logic and Algebraic Programming 78, no. 5, pp. 293-303, 2009.


J. Levy, S. Hassen, and T.E. Uribe. Combining Monitors for Runtime System. Electronic Notes in Theoretical Computer Science 70, no. 4, pp. 112-127, 2002.


J. Lukasiewicz. On three-valued logic. In L. Borkowski (ed.), Selected works by Jan Lukasiewicz, North–Holland, Amsterdam, pp. 87–88, 1920. ISBN 0-7204-2252-3.


Modelica Association. Modelica, A Unified Object-Oriented Language for Systems Modeling. Language Specification, Version 3.3, May 9, 2012. https://www.modelica.org/documents/ModelicaSpec33.pdf


OMG. Requirements Interchange Format (ReqIF), 2013. Download: http://www.omg.org/spec/ReqIF/1.1/PDF/ http://www.omg.org/spec/ReqIF/20110401/reqif.xsd


Open Source Modelica Consortium. OpenModelica, 2015. https://openmodelica.org/


M. Otter M, L. Buffoni, P. Fritzson, M. Sjölund, W. Schamai, A. Garro, A. Tundis, and H. Elmqvist. D2.1.1 – Modelica extensions for properties modelling, Part IV: Modelica for properties modeling. Internal report, ITEA2 MODRIO project, Sept. 2014.


N. Rescher. Many-valued Logic, McGraw-Hill, 1969.


W. Schamai. Model-Based Verification of Dynamic System Behavior against Requirements: Method, Language, and Tool. Ph.D. Thesis, No. 1547, University of Linköping, 2013.. Download: http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-98107


W. Schamai, L. Buffoni, and P. Fritzson. An Approach to Automated Model Composition Illustrated in the Context of Design Verification. Journal of Modeling, Identification and Control, volume 35- 2, pages 79—91, 2014.


S. Steinhorst and L. Hedrich . Targeting the Analog Verification Gap: State Space-based Formal Verification Approaches for Analog Circuits. CAV 2009, Grenoble, France, 2009. Download http://www.em.cs.unifrankfurt.de/FAC09/papers/FAC_09_Steinhorst.pdf


N. Thuy. D8.1.3 – Part 1 The Backup Power Supply. Internal report, ITEA2 MODRIO project, Nov. 2013.


N. Thuy. D2.1.1 – Modelica extensions for properties modelling, Part III: FOrmal Requirements Modelling LAnguage (FORM-L). Internal report, ITEA2 MODRIO project, Sept. 2014.


M. Tunnat. Integration modellbasierter Methoden in den Entwicklungsprozess hybrider Flugzeugregelungssysteme am Beispiel des Ventilation-Control-System. Master thesis, Technical University Hamburg-Harburg, Institut fĂĽr Flugzeug-Kabinensysteme, 2011.

Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015

Author:
Martin Otter, Nguyen Thuy, Daniel Bouskela, Lena Buffoni, Hilding Elmqvist, Peter Fritzson, Alfredo Garro, Audrey Jardin, Hans Olsson, Maxime Payelleville, Wladimir Schamai, Eric Thomas, Andrea Tundis
Title:
Formal Requirements Modeling for Simulation-Based Verification
DOI:
http://dx.doi.org/10.3384/ecp15118625
Note: the following are taken directly from CrossRef
Citations:
No citations available at the moment


Responsible for this page: Peter Berkesand
Last updated: 2017-02-21