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.