Abstract
In the development process the very first phase focuses on the requirements. Most of the requirements are dynamic and describe how the system reacts to a set of stimuli. Not all the possible reactions are listed in the requirements but some mandatory reactions are described that can be seen as properties. Later in the development process is a real system or a representative model of the future system. At that point it is possible to gather execution traces of the real system. Based on the work of the European PRESTO project this paper describes the work that has been done to use the same kind of model in both cases and match one against the other.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Compare, D., Inverardi, P., Pelliccione, P., Sebastiani, A.: Integrating model-checking architectural analysis and validation in a real software life-cycle. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 114–132. Springer, Heidelberg (2003)
Holzmann, G.J.: The SPIN Model Checker – Primer and Reference Manual. Addison Wesley (2003)
Holzmann, G.J.: The logic of bugs. In: Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 2002/FSE 2002, pp. 81–87. ACM (2002)
Muscholl, A., Peled, D.: Deciding Properties of Message Sequence Charts. In: Leue, S., Systä, T.J. (eds.) Scenarios. LNCS, vol. 3466, pp. 43–65. Springer, Heidelberg (2005)
Babica, J.: Message Sequence Charts properties and checking algorithms. Master Thesis at Masarykova Univerzita Fakulta Informatiky Brno (2009), http://scstudio.sourceforge.net/files/thesis_babica09.pdf
Brill, M., Damm, W., Klose, J., Westphal, B., Wittke, H.: Live Sequence Charts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 374–399. Springer, Heidelberg (2004)
Specification & Description Language - Real-Time (2006), http://www.sdl-rt.org/
Internation Telecommuication Union: Recommendation Z.120 (02/11) Message Sequence Chart (MSC), http://www.itu.int/rec/T-REC-Z.120
Autili, M., Inveradi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Automated Software Engineering 14(3), 293–340 (2007)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering, ICE 1999, pp. 411–420. IEEE Computer Society (1999)
PragmaDev Tracer, http://www.pragmadev.com/product/tracing.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gaudin, E., Brunel, E. (2013). Property Verification with MSC. In: Khendek, F., Toeroe, M., Gherbi, A., Reed, R. (eds) SDL 2013: Model-Driven Dependability Engineering. SDL 2013. Lecture Notes in Computer Science, vol 7916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38911-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-38911-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38910-8
Online ISBN: 978-3-642-38911-5
eBook Packages: Computer ScienceComputer Science (R0)