Mapping AADL to Petri Net Tool-Sets Using PNML Framework

Hassan Reza, Amrita Chatterjee

Department of Computer Science, School of Aerospace Sciences, University of North Dakota, Grand Forks, USA.

DOI: 10.4236/jsea.2014.711082                

Abstract

Architecture Analysis and Design Language (AADL) has been utilized to specify and verify nonfunctional properties of Real-Time Embedded Systems (RTES) used in critical application systems. Examples of such critical application systems include medical devices, nuclear power plants, aerospace, financial, etc. Using AADL, an engineer is enable to analyze the quality of a system. For example, a developer can perform performance analysis such as end-to-end flow analysis to guarantee that system components have the required resources to meet the timing requirements relevant to their communications. The critical issue related to developing and deploying safety critical systems is how to validate the expected level of quality (e.g., safety, performance, security) and functionalities (capabilities) at design level. Currently, the core AADL is extensively applied to analyze and verify quality of RTES embed in the safety critical applications. The notation lacks the formal semantics needed to reason about the logical properties (e.g., deadlock, livelock, etc.) and capabilities of safety critical systems. The objective of this research is to augment AADL with exiting formal semantics and supporting tools in a manner that these properties can be automatically verified. Toward this goal, we exploit Petri Net Markup Language (PNML), which is a standard acting as the intermediate language between different classes of Petri Nets. Using PNML, we interface AADL with different classes of Petri nets, which support different types of tools and reasoning. The justification for using PNML is that the framework provides a context in which interoperability and exchangeability among different models of a system specified by different types of Petri nets is possible. The contributions of our work include a set of mappings and mapping rules between AADL and PNML. To show the feasibility of our approach, a fragment of RT-Embedded system, namely, Cruise Control System has been used.

Keywords

Model-Based Engineering, Petri Nets, AADL, PNML, Software Architecture, Formal Methods

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	ISO/IEC 15909-2 (2011) Systems and Software Engineering—High-Level Petri Nets—Part 2: Transfer Format.
[2]	Hillah, L., Kordon, F., Petrucci, L. and Trèves, N. (2005) Model Engineering on Petri Nets for ISO/IEC 15909-2: API Framework for Petri Net Type Metamodels. Petri Net Newsletter, 69, 22-40.
[3]	Hillah, L.M., Kordon, F., Petrucci, L. and Trèves, N. (2010) PNML Framework: An Extendable Reference Implementation of the Petri Net Markup Language. In: Lilius, J. and Penczek, W., Eds., Petri Nets, LNCS, Vol. 6128, Springer, Heidelberg, 318-327.
[4]	Hillah, L., Kindler, E., Kordon, F., Petrucci, L. and Treves, N. (2009) A Primer on the Petri Net Markup Language and ISO/IEC 15909-2. In: Jensen, K., Ed., The 10th International Workshop on Practical Use of Colored Petri Nets and the CPN Tools (CPN 2009), 101-120.
[5]	Hillah, L., Kordon, F., Petrucci, L. and Trèves, N. (2006) PN Standardization: A Survey. 26th International Conference on Formal Methods for Networked and Distributed Systems (FORTE’06), Paris, 26-29 September 2006, 307-322.
[6]	Van der Werf, J.M.E.M. and Post, R.D.J. (2004) EPNML 1.1: An XML Format for Petri Nets (External Report). Petriweb.org, Eindhoven, 16.
[7]	Weber, M. and Kindler, E. (2002) The Petri Net Markup Language. In: Ehrig, H., Reisig, W., Rozenberg, G. and Weber, H. (Eds.), Petri Net Technology for Communication Based Systems, Vol. 2472 of Lecture Notes in Computer Science (LNCS), Springer-Verlag, Heidelberg, 124-144.
[8]	Reza, H. and Grant, E. (2009) Toward Extending AADL-OSATE Toolset with Color Petri Nets (CPNs). Proceeding of the Internal Conference on Information Technology: New Generations (ITNG’09), Las Vegas, 27-29 April 2009, 1085-1088.
[9]	Feiler, P.H., Gluch, D.P. and Hudak, J.J. (2006) The Architecture Analysis & Design Language (AADL): An Introduction. Technical Report, CMU/SEI-2006-TN-011.
[10]	XSL Transformations (XSLT) Version 1.1. http://www.w3.org/TR/xslt11/
[11]	Hudak, J. and Feiler, P. (2007) Developing AADL Models for Control Systems: A Practitioner’s Guide. Technical Report CMU/SEI-2007-TR-014, Software Engineering Institute, Carnegie Mellon University, Pittsburgh.
[12]	Murata, T. (1989) Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77, 541-580. http://dx.doi.org/10.1109/5.24143
[13]	Renault, X., Kordon, F. and Hugues, J. (2009) From AADL Architectural Models to Petri Nets: Checking Model Viability. 12th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC’09), Tokyo, 17-20 March 2009, 313-320.
[14]	Renault, X., Kordon, F. and Hugues, J. (2009) Adapting Models to Model Checkers, a Case Study: Analyzing AADL Using Time or Colored Petri Nets. IEEE International Workshop on Rapid System Prototyping, Paris, 23-26 June 2009, 26-33.
[15]	Chkouri, M.Y., Robert, A., Bozga, M. and Sifakis, J. (2008) Translating AADL into BIP—Application to the Verification of Real-Time Systems. In: Chaudron, M., Ed., Model Based Architecting and Construction of Embedded Systems, Springer-Verlag, Heidelberg, 5-19.
[16]	Gasevic, D. and Devedzic, V. (2003) Petri Net Markup Languages and Formats as Guidelines for Ontology Development. Proceedings of the IADIS International Conference on E-Society, Lisbon, 3-6 June 2003, 662-665.
[17]	Jin, Z. (2000) A Software Architecture-Based Testing Technique. Thesis for Doctor of Philosophy in Information Technology, George Mason University, Fairfax.
[18]	Technical and Historical Overview of MetaH. http://aadl.sei.cmu.edu/aadl/documents/Technical%20and%20Historical%20Overview%20of%20MetaH.pdf
[19]	Reza, H., Gu, F.F. and Shafai, B. (2010) Toward Model Based Testing: Combining AADLS with High Level Petri Nets. Software Engineering Research and Practice. CSREA Press, Las Vegas, 619-623.
[20]	Reza, H. and Lande, S. (2010) Model Based Testing Using Software Architecture. Seventh International Conference on Information Technology: New Generations (ITNG), Las Vegas, 12-14 April 2010, 188-193.
[21]	Jean-Paul, B., Rapha?l, C., David, C., Mamoun, F. and Jean-Fran?ois, R. (2007) A Mapping from AADL to Java-RTSJ. International Workshop on Java Technologies for Real-Time and Embedded Systems, Vienna, 26-28 September 2007, 165-174.
[22]	Dong, C. and Bailey, J. (2004) Static Analysis of XSLT Programs. Proceedings of the 15th Australasian Data Base Conference, 27, 151-160.
[23]	Tongprasert, K. and Chittayasothorn, S. (2010) An XML-Based Petri Net to Rules Transformation Software Tool. The 14th World Multi-Conference on Systemic, Cybernetics and Informatics: WMSCI 2010, Orlando Florida, 29 June-02 July 2010, 1-4.
[24]	Jensen, K., Kristiansen, L.M. and Wells, L. (2007) Colored Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer, 9, 213-254. http://dx.doi.org/10.1007/s10009-007-0038-x
[25]	Hecht, M., Vogle, C. and Lam, A. (2009) Application of the Architectural Analysis and Design Language (AADL) for Quantitative System Reliability and Availability Modeling. Aerotech 2009, Seattle, 30 August-2 September 2010, 1-15.
[26]	Singhoff, F., Legrand, J., Nana, L. and Marce, L. (2005) Scheduling and Memory Requirements Analysis with AADL. Proceedings of the 2005 Annual ACM SIGAda International Conference on Ada: The Engineering of Correct and Reliable Software for Real-Time and Distributed Systems Using Ada and Related Technologies, 25, 1-10.
[27]	Lassen, K.B. and Westergaard, M. (2006) Embedding Java Types in CPN Tools. Transactions on Petri Nets and Other Models of Concurrency, Aarhus, 24-26 October 2006, 1-19.
[28]	Bonnefoi, F., Choppy, C. and Kordon, F. (2009) A Discretization Method from Colored to Symmetric Nets: Application to an Industrial Example. Transactions on Petri Nets and Other Models of Concurrency III Lecture Notes in Computer Science, 5800, 159-188.
[29]	Reza, H., Gu, F. and Askelson, M. (2011) Model Based Engineering of Ground Based Risk Mitigation System. Proceedings of the 2011 International Conference on Software Engineering Research & Practice, Las Vegas, 18-21 July 2011, 260-265.
[30]	Lewis, B. and Feiler, P. (2008) Multi-Dimensional Model-Based Engineering Using AADL. The 19th IEEE/IFIP International Symposium on Rapid System Prototyping (RSP’08), Monterey, 2-5 June 2008, 15-18.
[31]	Knight, J.C. (2002) Safety Critical Systems: Challenges and Directions. Proceedings of the International Conference on Software Engineering, ICSE 2002, Orlando, 25 May 2002, 547-550.
[32]	Shaw, M. and Garlan, D. (1996) Software Architecture: Perspectives on an Emerging Discipline. Prentice Hall, Upper Saddle River.
[33]	Medvidovic, N. and Taylor, R. (2000) A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering, 26, 70-93. http://dx.doi.org/10.1109/32.825767
[34]	Feiler, P. and Gluch, D. (2013) Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. SEI Series, Addison Wesley, Boston.
[35]	Reza, H., Marsh, R. and Askelson, M. (2010) A Fault Tolerant Architecture Using AADLs and Error Model Annex for Unmanned Aircraft Systems (UAS). Software Engineering Research and Practice, CSREA Press, Las Vegas, 180-184.
[36]	Kindler, E. (2006) Concepts, Status, and Future Directions. In: Schnieder, E., Ed., EKA 2006, Braunschweig, 29-31 May 2006, 35-55.
[37]	Chow, F. (2013) Intermediate Representation. Communication of ACM, 56, 57-62. http://dx.doi.org/10.1145/2534706.2534720