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