| Abstract: |
Industrial embedded real-time systems such as cabin communication systems (CCS) of modern (passenger) aircrafts [EADS:08a], are highly complex. Verification of such complex systems is either
hampered by the state space explosion problem, --attached to state-based verification,-- or lacks a high-degree of detail, --due to the usage of some analytic method. For achieving a detailed
analysis of system components, but still maintaining scalability of the procedure for computing overall properties of a system, our current research tackles the combination of executable and
analytic model descriptions for the joint analysis of embedded real-time systems. As first step this report focuses on a combination of Timed Automata [AD:90a] with the MPA-method [CKT:03a],
where the latter is a relatively new compositional, analytical performance evaluation method based on the well-known Network Calculus [BT:01a]. As major outcome we present an efficient approach
for converting analytic (sub-)model descriptions of the MPA-method into networks of interacting Timed Automata. |
