Formal Requirements Modeling for Simulation-Based Verification

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

Ladda ner artikelhttp://dx.doi.org/10.3384/ecp15118625

Ingår i: Proceedings of the 11th International Modelica Conference, Versailles, France, September 21-23, 2015

Linköping Electronic Conference Proceedings 118:67, s. 625-635

Visa mer +

Publicerad: 2015-09-18

ISBN: 978-91-7685-955-1

ISSN: 1650-3686 (tryckt), 1650-3740 (online)


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.


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


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-

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.

Citeringar i Crossref