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 artikel
http://dx.doi.org/10.3384/ecp15118625Ingå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
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-
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.
