Technical reports

The transition assertions specification method

Victor A. Carreño

December 1992, 18 pages

DOI: 10.48456/tr-279

Abstract

A modelling and specification method for real-time, reactive systems is described. Modelling is performed by constructing time dependent relations of the system parameters. A textual formal notation using higher order logic and a graphical notation are presented. The formal notation allows the use of rigorous mathematical methods on the specification, one of the primary sources of design errors. A cruise control case example is included in the paper and the HOL mechanised theorem prover is used to show that the specification comply with some top level requirements.

Full text

PDF (1.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-279,
  author =	 {Carre{\~n}o, Victor A.},
  title = 	 {{The transition assertions specification method}},
  year = 	 1992,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-279.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-279},
  number = 	 {UCAM-CL-TR-279}
}