@article{Andersen_Kristensen_Skou_1995, title={Specification and Automated Verification of Real-Time Behaviour —A Case Study}, volume={2}, url={https://tidsskrift.dk/brics/article/view/19961}, DOI={10.7146/brics.v2i60.19961}, abstractNote={<p>In this paper we sketch a method for specification and automatic<br />verification of real-time software properties. The method combines<br />the IEC 848 norm and the recent specification techniques TCCS (Timed<br />Calculus of Communicating Systems) and TML (Timed Modal Logic)<br /> - supported by an automatic verification tool, Epsilon. The method<br />is illustrated by modelling a small real-life steam generator example and<br />subsequent automated analysis of its properties.</p><p><br />Keywords: Control system analysis; formal specification; formal verification; real-time systems; standards.</p>}, number={60}, journal={BRICS Report Series}, author={Andersen, Jørgen H. and Kristensen, Carsten H. and Skou, Arne}, year={1995}, month={Jun.} }