Abstract
Developing correct concurrent software is challenging. Design errors can result in deadlocks, race conditions and livelocks, and discovering these is difficult. A serious obstacle for an industrial uptake of rigorous analysis techniques such as model checking is the learning curve associated to the languages — typically temporal logics — used for specifying the application-specific properties to be checked. To bring the process of correctly eliciting functional properties closer to software engineers, we introduce PASS, a Property ASSistant wizard as part of a UML-based front-end to the mCRL2 toolset. PASS instantiates pattern templates using three notations: a natural language summary, a μ-calculus formula and a UML sequence diagram depicting the desired behavior. Most approaches to date have focused on LTL, which is a state-based formalism. Conversely, μ-calculus is event-based, making it a good match for sequence diagrams, where communication between components is depicted. We revisit a case study from the Grid domain, using PASS to obtain the formula and monitor for checking the property.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Remenska, D., Templon, J., Willemse, T.A.C., Homburg, P., Verstoep, K., Casajus, A., Bal, H.: From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 244–260. Springer, Heidelberg (2013)
Groote, J., et al.: The Formal Specification Language mCRL2. In: Proc. MMOSS 2006 (2006)
Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. In: Science of Computer Programming (2005)
Dwyer, M.B., et al.: Patterns in property specifications for finite-state verification. In: Proc. ICSE 1999 (1999)
Dwyer, M.B., et al.: Property Specification Patterns, http://patterns.projects.cis.ksu.edu
Smith, R.L., et al.: Propel: an approach supporting property elucidation. In: Proc. ISCE 2002 (2002)
Konrad, S., Cheng, B.H.: Facilitating the construction of specification pattern-based properties. In: Proc. RE 2005. IEEE (2005)
Mondragon, O., Gates, A.Q., Roach, S.: Prospec: Support for Elicitation and Formal Specification of Software Properties. In: Proc. of Runtime Verification Workshop. ENTCS (2004)
Autili, M., Inverardi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Automated Software Eng. (2007)
Lee, I., Sokolsky, O.: A Graphical Property Specification Language. In: Proc. of 2nd IEEE Workshop on High-Assurance Systems Engineering (1997)
Smith, M.H., et al.: Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs. In: Proc. RE 2001 (2001)
Knapp, A., Wuttke, J.: Model checking of UML 2.0 interactions. In: Kühne, T. (ed.) MoDELS 2006. LNCS, vol. 4364, pp. 42–51. Springer, Heidelberg (2007)
Lilius, J., Paltor, I.P.: vUML: a Tool for Verifying UML Models. In: Proc. ASE 1999 (1999)
Kugler, H.-J., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005)
Baresi, L., Ghezzi, C., Zanolin, L.: Modeling and Validation of Publish/Subscribe Architectures. In: Testing Commercial-off-the-Shelf Components and Systems. Springer, Heidelberg
The Eclipse Foundation: Eclipse Modeling MDT-UML2 component, http://www.eclipse.org/uml2/
Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proc. ASE 2001 (2001)
Emerson, E.A.: Model checking and the Mu-calculus. In: DIMACS Series in Discrete Mathematics. American Mathematical Society (1997)
Cranen, S., Groote, J.F., Reniers, M.: A linear translation from CTL* to the first-order modal μ-calculus. Theoretical Computer Science (28) (2011)
OMG: UML2.4 Superstructure Spec., http://www.omg.org/spec/UML/2.4/Superstructure
Harel, D., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software & Systems Modeling 7 (2008)
Mateescu, R.: Property Pattern Mappings for Regular Alternation-Free μ-Calculus, http://www.inrialpes.fr/vasy/cadp/resources/evaluator/rafmc.html
Bauer, A.: Monitorability of omega-regular languages. CoRR abs/1006.3638 (2010)
Remenska, D., Willemse, T.A.C.: PASS: Property ASSistant tool for Eclipse, https://github.com/remenska/PASS
Tsaregorodtsev, A., et al.: DIRAC: A Community Grid Solution. In: Proc. CHEP 2007. IOP Publishing (2007)
Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81–95. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Remenska, D., Willemse, T.A.C., Templon, J., Verstoep, K., Bal, H. (2014). Property Specification Made Easy: Harnessing the Power of Model Checking in UML Designs. In: Ábrahám, E., Palamidessi, C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2014. Lecture Notes in Computer Science, vol 8461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43613-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-662-43613-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43612-7
Online ISBN: 978-3-662-43613-4
eBook Packages: Computer ScienceComputer Science (R0)