Issue No. 09 - September (1992 vol. 18)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.159838
<p>A layered approach to the specification and verification of real-time systems is described. Application processes are specified in the CSR Application Language, which includes high-level language constructs such as timeouts, deadlines, periodic processes, interrupts, and exception handling. A configuration schema is used to map the processes to system resources, and to specify the communication links between them. The authors automatically translate the result of the mapping into the CCSR process algebra, which characterizes CSR's resource-based computation model by a prioritized transition system. For the purposes of verification, a reachability analyzer based on the CCSR semantics has been implemented. This tool mechanically evaluates the correctness of the CSR specification by checking whether an exception state can be reached in its corresponding CCSR term. The effectiveness of this technique is illustrated by a multisensor robot example.</p>
layered approach; specification; verification; real-time systems; CSR Application Language; high-level language constructs; timeouts; deadlines; periodic processes; interrupts; exception handling; configuration schema; system resources; communication links; CCSR process algebra; resource-based computation model; prioritized transition system; reachability analyzer; CCSR semantics; correctness; exception state; multisensor robot example; calculus of communicating systems; exception handling; formal specification; formal verification; high level languages; real-time systems
R. Gerber and I. Lee, "Guest A Layered Approach to Automating the Verification of Real-Time Systems," in IEEE Transactions on Software Engineering, vol. 18, no. , pp. 768-784, 1992.