ASTRAL SPECIFICATION FOR A RAILROAD CONTROLLER
L.J.G. Bun, J. van Katwijk · 1995
It is generally accepted that development of requirement models for real-time systems benefits from formal specifications. In order to be able to evaluate notations for use in the development of real-time software systems, we are performing a comparative review of some selected specification notations. The study emphasizes the use of the notations in the domain of real-time (control) applications. Our review will be based on a specification from a simple railroad controller model. This case contains data modelling aspects, functional aspects as well as temporal aspects. A (toy) railroad with a computer interface, is available in our laboratory, used for lab assignments. Typical elements to consider are usability with regard to the specification in relation to the requirements, and second, usability with respect to further program development. This report discusses the problem as well as a model specification, written in Astral. It also discusses verification issues using the proof assi...