HP Labs Technical Reports

History Specifications

Harry, Paul

HPL-91-34

Keyword(s):

Abstract: This paper defines a style of relational specification, called history specification, in which whole histories, rather than merely individual values, of inputs and outputs are related. Each relation between histories is termed a process; these processes can be composed together to give a hierarchical specification. The processes may be specified entirely textually, in a formal language such as HP-SL, or more conveniently by a mixed graphical and textual notation. This mixed notation resembles the mixed graphical and textual notation. This mixed notation resembles the dataflow diagrams used in real-time extensions to structured analysis. History specifications may either be viewed as a way to structure formal specifications, or as a way to formalise dataflow diagrams. They have been successfully used industrially to specify a real time embedded system.

Back to Index