Toward Extending AADL-OSATE Toolset with Color Petri Nets (CPNs)

Architectural Analysis and Description Languages (AADLs), a model-based engineering notation, and its supporting toolset, Open Source Architectural Tool Environment (OSATE) are industry standard under the Society of Automotive Engineering (SAE). AADL-OSATE has shown significant promises in the development of highly sophisticated systems. As such, it has been adopted to specify and analyze real-time embedded systems used in the domain of safety critical systems. By using AADL-OSATE, designers are able to specify, analyze, and/or predicate the system-wide properties such as safety, performance, reliability, security, availability, etc. Examples of application systems developed in AADL-OSATE include avionics and aerospace, and manufacturing system. This main shortcoming of AADL-OSTATE is that it is difficult for analyzing the behaviors of components (processes/threads) in ways that deadlock and/or livelock can be detected. To this end, we are proposing to extent the capabilities of AADL-OSATE modeling notation and supporting tool set with Petri nets in a manner that facilitates formal analysis to verify the absence of deadlock and/or livelock phenomenon.