VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems
Duncan L. Clarke, Insup Lee, Hong-Liang Xie · 1993
VERSA is a tool that assists in the algebraic analysis of real-time systems. It is based on ACSR, a timed process algebra designed to express resource-bound real-time distributed systems. VERSA supports the analysis of real-time processes through algebraic rewriting, interactive execution, and equivalence testing. This paper begins by presenting a brief overview of the process algebra ACSR, its syntax, operational semantics, and equivalence relations. VERSA's process and command syntax, its algebraic rewrite system, and its state-based analysis features are described fully. The presentation includes examples that illustrate the salient features of ACSR, and output from sample VERSA sessions that demonstrate the application of the tool to real-time systems analysis. 1 Introduction Reliability in real-time systems can be improved through the use of formal methods for the specification and analysis of real-time systems. Formal methods treat system components as mathematical objects and p...