ADL: An Activity Description Language for Real-Time Networks

Abstract

Abstract. This paper introduces and motivates ADL, a new formal notation for the specification of the temporal and functional behaviour of concurrent processes. ADL is tailored to be directly compatible with the DORIS design method. It combines a graphical Activity State-Machine (ASM) notation and a model-based Activity Functional Behaviour (AFB) notation. The abstract syntax, and static and dynamic semantics for the ASM notation are given, the dynamic semantics being given proof-theoretically in many-sorted logic extended with the RTL ‘occurrence’ relation, Θ , and the ERTL ‘holding’ relation, Φ . ADL is used to specify a small network, and proofs are given of its timeliness and safety properties.