Formally specifying CARA in Java

A restricted dialect of Java is proposed as a language for writing formal specifications for reactive systems. Specifications written in this dialect have one Java class per system module. Each class uses static fields to record module state, uses synchronized static methods as entry points for services provided by the module, and communicates with other modules by method calls. Specifications written in this form are directly executable, can serve as a reference model for subsequent implementations, and can also be used as a target for formal verification techniques. Application of the method to construct an executable specification of the CARA (Computer-Assisted Resuscitation Algorithm) system is described.