A layered approach to automating the verification of real-time systems

摘要

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.