Article | Proceedings of the 10<sup>th</sup> International Modelica Conference; March 10-12; 2014; Lund; Sweden | Making Modelica Applicable for Formal Methods
Göm menyn

Title:
Making Modelica Applicable for Formal Methods
Author:
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
DOI:
10.3384/ecp14096205
Download:
Full text (pdf)
Year:
2014
Conference:
Proceedings of the 10th International Modelica Conference; March 10-12; 2014; Lund; Sweden
Issue:
096
Article no.:
021
Pages:
205-211
No. of pages:
7
Publication type:
Abstract and Fulltext
Published:
2014-03-10
ISBN:
978-91-7519-380-9
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

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.

Keywords: Qualitative reasoning; formal methods; model reuse; declarative models

Proceedings of the 10th International Modelica Conference; March 10-12; 2014; Lund; Sweden

Author:
Matthew Klenk, Daniel G. Bobrow, Johan de Kleer, Bill Janssen
Title:
Making Modelica Applicable for Formal Methods
DOI:
http://dx.doi.org/10.3384/ecp14096205
References:

[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.

Proceedings of the 10th International Modelica Conference; March 10-12; 2014; Lund; Sweden

Author:
Matthew Klenk, Daniel G. Bobrow, Johan de Kleer, Bill Janssen
Title:
Making Modelica Applicable for Formal Methods
DOI:
http://dx.doi.org/10.3384/ecp14096205
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