BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/javacara.pdf
       ENTRY:: October 3, 2002
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Formally Specifying CARA in Java
        TYPE:: Technical Report
      AUTHOR:: Eugene W. Stark
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 631-632-8444 <stark@cs.sunysb.edu>
        DATE:: October 3, 2003
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~pioa/Papers/javacara.abstract

ABSTRACT::

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.