ADL: An Activity Description Language for Real-Time Networks

摘要

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.