Specification

We started with a state machine written as a series of transitions in an Excel file. Each line of the file corresponds to a single transition, and columns contain start states, destination states, guards, and actions. There are two files; the first one has the main component and the second includes the alarm component and several smaller components.

The Excel files were translated into the extended finite state machine (EFSM) format. The file here contains all of the state machines as a single communicating EFSM system.

The EFSM was then in turn translated into an input file for the UPPAAL model checker. UPPAAL allows us to check properties of the system and simulate its behavior.

• Excel file 1 and file 2 with state machine specification
• CSV file with state machine specification
• EFSM format state machine
• UPPAAL model of specification

Generic PCA model

• Model documentation
• Model files (tgz archive)

The revisions are in progress and updated versions will be posted as they become available.

We are currently developing a reference implementation of GPCA.