Formal verification of AADL behavior models: a feasibility investigation

ABSTRACT

OSATE is an open source platform and toolset built upon Eclipse plug-in technology that supports the modeling and analysis of real-time reactive systems. OSATE implements the Society Automotive Engineers (SAE) standard Architecture Analysis & Design Language (AADL). Because many real-time reactive systems are safety-critical and mission-oriented, the behaviors of these systems are typically subtle and intricate such that even an experienced designer faces significant challenges in their correct design. An AADL Behavior Annex is being developed to help engineers in addressing these challenges. Since several formal model-checking tools have shown the capability of tracing and verifying temporal logic properties of reactive systems, it is desirable to integrate these tools into the OSATE toolset. This will enable the formal verification of the behavior of AADL models. In this paper, we present two case studies that explore the feasibility of extending model-checking tools to the OSATE toolset. The preliminary work and case studies in this paper address several important questions relating to a tool integration project.

REFERENCES

• 1: Feiler, Peter H.; Gluch, David P.; Hudak, The Architecture Analysis&Design Language (AADL): An Introduction, (CMU/SEI-2006-TN-011), Pittsburgh, Pa.: Software Engineering Institute, Carnegie Mellon University, Feb. 2006.
• 2: The SAE Architecture Analysis&Design Language (AADL) www.aadl.info.
• 3: Ricardo Bedin Franca , Jean-Paul Bodeveix , Mamoun Filali , Jean-Francois Rolland , David Chemouil , Dave Thomas, The AADL behaviour annex -- experiments and roadmap, Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems, p.377-382, July 11-14, 2007 [doi>10.1109/ICECCS.2007.41]
• 4: Ricardo Bedin Fran, ca, Jean-Fran, cois Rolland, Mamoun Filali Amine, Jean-Paul Bodeveix, Assessment of the AADL Behavioral Annex, www.cert.fr/feria/svf/FAC/2007/Papiers/11.pdf
• 5: The Topcased Team, OSATE-BA. org.topcased.aadl.behavior_0.5.0, http://gforge.enseeiht.fr/frs/?group id=37.
• 6: Annex Behavior_Specification V1.6, SAE AS5506, aero. la.sei.cmu.edu/aadl/documents/Behaviour_Annex1.6.pdf}
• 7: Comella-Dorda, S.; Gluch, D. P.; Hudak, J.; Lewis, G; and Weinstock, C., Model-Based Verification -- Claims Generation Guidelines: Software Engineering, Institute technical note: CMU/SEI-2001-TN-018, October 2001. {http://www.sei.cmu.edu.publications/documents/01.reports/01tn018.html}
• 8: Liu, H.&Gluch, D. P. Query Generation Guidelines and Consideration to Statecharts of Object-Oriented Designs, Proceeding of the Conference of Advances in Computer Sciences and Technology sponsored by IASTED, Nov, 2004.
• 9: Hong Liu , David P. Gluch, Conceptual modeling with the object-process methodology in software architecture, Journal of Computing Sciences in Colleges, v.19 n.3, p.10-21, January 2004
• 10: Hong Liu , David P. Gluch, Templates and automation for temporal query generation, Proceedings of the 44th annual Southeast regional conference, March 10-12, 2006, Melbourne, Florida [doi>10.1145/1185448.1185467]
• 11: NuSMV, 2.4 free download http://nusmv.itc.it/, tutorial, http://nusmv.fbk.eu/NuSMV/tutorial/index.html
• 12: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 13: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 14: Gerd Behrmann, Alexandre David, and Kim G. Larsen, A Tutorial on Uppaal and UPPAAL 4.06, free download, www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf, http://www.uppaal.com/.
• 15: Anouck Renée Girard, João Borges de Sousa, James A. Misener and J. Karl Hedrick, A "Control Architecture for Integrated Cooperative Cruise Control and Collision Warning Systems", path.berkeley.edu/~anouck/papers/cdc01inv3102.pdf.
• 16: Dionisio de Niz , Peter H. Feiler, Aspects in the industry standard AADL, Proceedings of the 10th international workshop on Aspect-oriented modeling, p.15-20, March 12-12, 2007, Vancouver, Canada [doi>10.1145/1229375.1229378]
• 17: Shriram Krishnamurthi , Kathi Fisler, Foundations of incremental aspect model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.2, p.7-es, April 2007 [doi>10.1145/1217295.1217296]
• 18: Rik Eshuis, Symbolic model checking of UML activity diagrams, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.1, p.1-38, January 2006 [doi>10.1145/1125808.1125809]
• 19: J.-P. Bodeveix1, M. Filali1, M. Rached, D. Chemouil, and P. Gaufillet, Experimenting an AADL Behavior Annex and a Verification Method, ftp://ftp.estec.esa.nl/pub/wm/wme/Web/AADLExperience2 006.pdf

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Languages, Verification

Keywords:
architecture analysis & design language, computational tree logic, model checking, tool integration