Abstract
This paper is a study of observer-based proof techniques applied to the verification of a model of a real world embedded system, an aircraft landing gear. We present a formal description of these techniques (taken from [5]) and look at three ways of applying them, comparing verification of the composed system with two approaches to decompositional verification. The example illustrates that due to the tight interaction in a plant-controller setting there is often little to be gained by adopting a decompositional approach to verification. Nonetheless, two reasons are presented for separation between the controller and its environment at the modelling stage. Hence the result of the study is that in cases similar to this one, it is most expedient to prove system properties using the composed model derived from individual parts.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing Specifications. In J.W. de Bakker, W.P. de Roever, and G.Rozenberg, editors, proceedings of the REX workshop on stepwise refinement of distributed systems, LNCS 430, pages 1–41. Springer Verlag, 1989.
A. Børjesson, K.G. Larsson, and A. Skou. Generality in Design and Compositional Verification Using TAV. Formal Methods in System Design, 6:239–258, 1995.
H. De-Leon and O. Grumberg. Modular Abstractions for Verifying Real-time Distributed Systems. Formal Methods in System Design, 2:7–43, 1993.
R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Proc. Workshop on Theory of Hybrid Systems, October 1992, LNCS 736, Lyngby, Denmark, 1993. Springer Verlag.
N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag.
L.J. Jagadeesan, C. Puchol, and J.E. Von Olnhausen. A Formal Approach to Reactive Systems Software: A Telecommunications Application in Esterel. Formal Methods in System Design, 8:123–151, 1996.
R. Kaivola. Compositional Model Checking for Linear-Time Temporal Logic. In Proc. 4th int. workshop on Computer Aided Verification, pages 248–259. Springer Verlag, 1992.
R. Milner. Communications and Concurrency. Prentice-Hall, 1989.
S. Nadjm-Tehrani and J-E. Strömberg. From physical modelling to compositional models of hybrid systems. In Proc. of the 3rd International Conference on Formal Techniques in Real-time and Fault-tolerant Systems, pages 583–604. LLNCS 863, Springer Verlag, 1995.
S. Nadjm-Tehrani and J-E. Strömberg. Proving dynamic properties in an aerospace application. In 16th International Symposium on Real-time Systems, pages 2–10. IEEE Computer Society Press, December 1995.
P.J.G. Ramadge and W.M. Wonham. The Control of Discrete Event Systems. Proceedings of the IEEE, 77:81–97, 1989.
Martin D. Westhead and John Hallam. Modelling hybrid systems as the limit of discrete computational processes. In International Conference on Robotics and Automation. IEEE, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Westhead, M., Nadjm-Tehrani, S. (1996). Verification of embedded systems using synchronous observers. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_53
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive