Abstract
Safety issues of cooperating embedded systems are very important since they are closely related to our living. In this research, modeling techniques and safety analysis techniques for cooperating embedded systems are provided. Behaviors of embedded systems and safety properties are described by Labeled Transition Systems (LTS). For convenient and effective analysis, we provide a slicing method of the state space of a system according to a property. Based on the slice models, we provided an equivalence algorithm of LTS models and a compositional analysis technique of safety properties.
Chapter PDF
Similar content being viewed by others
References
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Dordrecht (1993)
Avrunin, G.S., et al.: Automated analysis of concurrent systems with the constrained expression toolset. IEEE trans. software engineering 17(11), 1204–1222 (1991)
Cheung, S.C., Kramer, J.: Tractable dataflow analysis for distributed systems. IEEE trans. software engineering 20(8), 579–593
Dwyer, M.B., Clarker, L.A.: Data flow analysis for verifying properties of concurrent programs. In: Proc. of the 2nd ACM SIGSOFT Symposium on the foundation of software engineering, pp. 62–75. ACM Press, New York (1994)
Cheung, S.C., Kramer, J.: Context constraints for compositional reachability analysis. ACM trans. software engineering and methodology 5(4), 334–377 (1996)
Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Proc. of the 3rd international conference on computer aided verification (1991)
Long, D., Clarke, L.: Task interaction graphs for concurrency analysis. In: Proc. of the 11th ICSE, pp. 44–52 (1989)
Valmari, A., et al.: Putting advanced reachability analysis techniques together: The ‘ARA’ tool. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 597–616. Springer, Heidelberg (1993)
Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proc. of ACM SIGSOFT, pp. 49–59 (1991)
Cheung, S.C., Kramer, J.: Checking Safety Properties using Compositional Reachability Analysis. In: ACM TOSEM, pp. 49–78 (1999)
Malhotra, J., et al.: A tool for hierarchical design and simulation of concurrent systems. In: Proc. of the BCS-FACS workshop on specification and verification of concurrent systems, pp. 140–152 (1988)
Sabnani, K.K., et al.: An algorithmic procedure for checking safety properties of protocols. IEEE trans. communication 37(9), 940–948 (1989)
Tai, K.C., Koppol, P.V.: An incremental approach to reachability analysis of distributed programs. In: Proc. of the 7th international workshop on software specification and design, pp. 141–150 (1993)
Denning, P.J., et al.: Machines, Languages, and Computation. Prentice-Hall, Englewood Cliffs (1978)
Milber, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Lee, W.J., Kim, HJ., Chae, H.S. (2007). Safety Property Analysis Techniques for Cooperating Embedded Systems Using LTS. In: Obermaisser, R., Nah, Y., Puschner, P., Rammig, F.J. (eds) Software Technologies for Embedded and Ubiquitous Systems. SEUS 2007. Lecture Notes in Computer Science, vol 4761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75664-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-75664-4_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75663-7
Online ISBN: 978-3-540-75664-4
eBook Packages: Computer ScienceComputer Science (R0)