The executable specification language Requirements Specification Formalism (RSF) has been designed to specify systems with time constraints. The aim of this paper is to illustrate the expressive power of the language together with the features of its execution environment.

The specification is given in the form of a set of transition rules that express the flow of the data among a number of system components, along with the behavior and time constraints of the whole system. In particular, time constraints are given via explicit expressions involving time values. Properties of data are specified by predicates, which are defined in a logic programming style. Transformations of data are specified by functions that are encoded in a functional programming style.

RSF has been implemented on top of a Prolog system that has been extended and given the possibility of handling functional definitions. The execution environment provides rapid prototyping faculties that enable the user to check general properties of the behavior of the proposed system.

To illustrate the language, the paper presents a fully worked-out example for specifying a simple yet meaningful system. It provides diagrams for the system in the style of SA diagrams, and the RSF specifications state the essential features of the system. The paper gives details of the behavior of the system as an explanation of the rules.

RSF is currently under experimentation and is being used for specifying systems in which the notion of time passing is crucial. It has been used for specifying a patient monitoring system and an access control system that monitors access to a building.