Making Modelica Applicable for Formal Methods

Matthew Klenk
Palo Alto Research Center, Palo Alto, CA, USA

Daniel G. Bobrow
Palo Alto Research Center, Palo Alto, CA, USA

Johan de Kleer
Palo Alto Research Center, Palo Alto, CA, USA

Bill Janssen
Palo Alto Research Center, Palo Alto, CA, USA

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

Ingår i: Proceedings of the 10th International Modelica Conference; March 10-12; 2014; Lund; Sweden

Linköping Electronic Conference Proceedings 96:21, s. 205-211

Visa mer +

Publicerad: 2014-03-10

ISBN: 978-91-7519-380-9

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


Engineers need to perform many different types of analyses as they design systems. Modelica has become a leading language to support numerical simulation. As a consequence there is widespread understanding of Modelica and a large number of Modelica model libraries available. This paper addresses the task of using formal methods to derive system properties such as whether a design meets its requirements for all possible inputs. We report on our experience building a qualitative reasoner operating on Modelica models. In this paper; we highlight five Modelica modeling practices that impede the application of formal methods.


Qualitative reasoning; formal methods; model reuse; declarative models


[Carloni et al., 2006] Luca P Carloni, Roberto Passerone, and Alessandro Pinto. Languages and tools for hybrid systems design, volume 1. Now Pub, 006.

[de Kleer and Williams, 1991] J. de Kleer and B. C. Williams, editors. Qualitative Reasoning about Physical Systems II. Elsevier, Amsterdam, October 1991. Artificial Intelligence 51.

[de Kleer et al., 2013] Johan de Kleer, Bill Janssen, Daniel G. Bobrow, Tolga Kurtoglu, Bhaskar Saha, Nicholas R. Moore, and Saravan Sutharshana. Fault augmented modelica models. In 24th International Workshop on Principles of Diagnosis, pages 71–78, Jerusalem, Israel, 2013.

[Everett, 1999] John Otis Everett. Topological inference of teleology: Deriving function from structure via evidential reasoning 6. Artificial Intelligence, 113:149–202, 1999. DOI: 10.1016/S0004-3702(99)00049-1

[Forbus, 1984] K. D. Forbus. Qualitative process theory. Artificial Intelligence, 24(1):85–168, 1984. Also in: Bobrow, D. (ed.) Qualitative Reasoning about Physical Systems (North-Holland, Amsterdam, 1984 / MIT Press, Cambridge, Mass., 1985).

[Fritzson, 2004] P. Fritzson. Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Wiley-IEEE Press, Piscataway, NJ, 2004. DOI: 10.1109/9780470545669

[Klenk et al., 2012] Matthew Klenk, Johan de Kleer, Daniel G. Bobrow, Sungwook Yoon, John Hanley, and Bill Janssen. Guiding and verifying early design using qualitative simulation. In Proceedings of the ASME 2012 IDETC and CIE, Chicago, IL, 2012.

[Kuipers, 1994] Benjamin Kuipers. Qualitative reasoning: modeling and simulation with incomplete knowledge. MIT Press, Cambridge, MA, USA, 1994.

[Lundvall et al., 2004] Håkan Lundvall, Peter Bunus, and Peter Fritzson. Towards automatic generation of model checkable code from modelica. 2004.

[Mattsson et al., 2002] Sven Erik Mattsson, Hilding Elmqvist, Martin Otter, and Hans Olsson. Initialization of hybrid differential-algebraic equations in modelica 2.0. In 2nd Inter. Modelica Conference 2002, pages 9–15, 2002.

[Papadopoulos et al., 2012] Alessandro V Papadopoulos, Martina Maggio, Francesco Casella, Johan Åkesson, and AB Modelon. Function inlining in modelica models. In 7th Vienna Conference on Mathematical Modelling, 2012.

[Parrotto et al., 2010] Roberto Parrotto, Johan Åkesson, and Francesco Casella. An xml representation of dae systems obtained from continuous-time modelica models. In EOOLT, pages 91–98, 2010.

[Snooke and Price, 2012] Neal Snooke and Chris Price. Automated {FMEA} based diagnostic symptom generation. Advanced Engineering Informatics, 26(4):870–888, 2012. DOI: 10.1016/j.aei.2012.07.001

[Struss and Price, 2004] Peter Struss and Chris Price. Model-based systems in the automotive industry. AI Magazine, 24(4):17–34, 2004.

[Tiwari, 2012] Ashish Tiwari. Hybridsal relational abstracter. In CAV, pages 725–731, 2012.

[Weld and de Kleer, 1989] D.S. Weld and J. de Kleer. Readings in Qualitative Reasoning about Physical Systems. Morgan Kaufmann, 1989.

[Wetzel and Forbus, 2009] Jon Wetzel and Ken Forbus. Automated critique of sketched mechanisms. Proceedings of the 21st Innovative Applications of Artificial Intelligence Conference, Pasadena, CA, 2009.

Citeringar i Crossref