Real-Time Systems Group

The University of Pennsylvania

1. Application of rewriting rules to ACSR specifications to deduce system properties.
2. Construction of a state machine and automatic exploration and analysis of the state space to verify safety properties and test equivalence of alternative process formulations.
3. Interactive execution of the process specification to explore specific system behaviors and sample the execution traces of the system.

VERSA extends the basic ACSR syntax with a number of notational conventions borrowed from programming languages. Specifications can be broken up into logical components and recombined using file inclusion. Symbolic constants and macros can be defined using a #define notation similar to the C programming language. Indexed process variable names, resource names, and event labels are allowed. Indexed composition and set construction operators are provided for operating on sets of indexed names.

The basic VERSA system has a command oriented interface for inputting process descriptions, binding them to identifiers, and operating on them. There is also a version of VERSA with an X/Motif user interface known as X-VERSA. X-VERSA doesn't support indexed names, but it does provide a point-and-click interface that dramatically improves the usability of the algebraic term rewriting facility.

VERSA and X-VERSA are implemented in C++. The Lex and Yacc compiler construction tools, the LEDA class library, and the libg++ and X/Motif libraries were used extensively to enhance portability. The use of a low-level programming language and the most current algorithms state machine construction and bisimulation testing has resulted in performance that compares very favorably with existing process algebra analysis toolkits.

Obtaining VERSA

• versa Sun4 compiled version of the VERSA system.
• xversa Sun4 compiled VERSA with an X/Motif wrapper. To run, XAPPLRESDIR environment variable must point at a directory holding XVersa.
• XVersa Default resource file for X-VERSA. Must be in a directory pointed to by the XAPPLRESDIR environment variable to run X-VERSA.
• examples.tar Collection of example files for various classic and not-so-classic concurrency problems coded in ACSR/VERSA.
• nutshell.ps VERSA in a Nutshell. A short VERSA tutorial used in a course taught at Penn. Contains a few Penn-specific references that will have to be tailored to the local site.

References

• VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems. D. Clarke, I. Lee, and H. Xie, Journal of Computer and Software Engineering, 3(2), April 1995.
  
• VERSA: A Tool for Analyzing Resource-Bound Real-Time Systems. D. Clarke and I. Lee, Special session on models and formalisms for representing and reasoning about temporal phenomena, IEA/AEI '94, Austin, Texas, May 1994.
  
• VERSA: Verification, Execution and Rewrite System for ACSR. D. Clarke, University of Pennsylvania Technical Report MS-CIS-95-34, October 1995.
  

Examples

• Railroad Crossing Control Systems. ps file
  
• Two Robots Manufacturing System. description, ps file, acsr
  
• Schedulability Analyzer
  
• Airport Control System. description, acsr
  
• ATM. ps file
  
• Philips Audio Control Systems. description, acsr
  

Further Information

• About the Penn Real-Time Systems Group.
  
• About the Penn Computer and Information Science Department.
  
• About Penn's School of Engineering and Applied Science.
  
• About the University of Pennsylvania.
  
• About Automated Reasoning System Implementations.