Abstract
This paper proposes a formal approach for generating proof obligations to verify local invariants in an Algebraic State Transition Diagram (ASTD). ASTD is a graphical specification language that allows for the combination of extended hierarchical state machines using CSP-like process algebra operators. Invariants can be declared at any level in a specification (state, ASTD), fostering the decomposition of system invariants into modular local invariants which are easier to prove, because proof obligations are smaller. The proof obligations take advantage of the structure of an ASTD to use local invariants as hypotheses. ASTD operators covered are automaton, sequence, closure and guard. Proof obligations are discharged using Rodin. When proof obligations cannot be proved, ProB can be used to identify counter-examples to help in correcting/reinforcing the invariant or the specification.
This work was supported by the ANR projet DISCONT, Public Safety Canada and NSERC.
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
Similar content being viewed by others
Notes
References
de Azevedo Oliveira, D., Frappier, M.: Modelling an automotive software system with TASTD. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds.) Rigorous State-Based Methods (ABZ2023). LNCS, vol. 14010, pp. 124–141. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_10
de Azevedo Oliveira, D., Frappier, M.: TASTD: A real-time extension for ASTD. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P.A. (eds.) Rigorous State-Based Methods (ABZ2023). LNCS, vol. 14010, pp. 142–159. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_11
Cartellier, Q.: https://gitlab.com/QCartellier/icfem2023-poastd/-/tree/main/ (2023)
El Jabri, C., Frappier, M., Ecarot, T., Tardif, P.M.: Development of monitoring systems for anomaly detection using ASTD specifications. In: Aït-Ameur, Y., Crăciun, F. (eds.) TASE. LNCS, vol. 13299, pp. 274–289. Springer (2022). https://doi.org/10.1007/978-3-031-10363-6_19
Fayolle, T.: Combinaison de méthodes formelles pour la spécification de systèmes industriels. Theses, Université Paris-Est; Université de Sherbrooke, Québec, Canada, June 2017
Frappier, M., Gervais, F., Laleau, R., Fraikin, B., St-Denis, R.: Extending Statecharts with process algebra operators. ISSE 4(3), 285–292 (2008)
Khan, A.H., Rauf, I., Porres, I.: Consistency of UML class and Statechart diagrams with state invariants. In: MODELSWARD, pp. 14–24. SciTePress (2013)
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B Method. JSTTT 10(2), 185–203 (2008)
Mammar, A., Frappier, M.: Modeling of a speed control system using event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 367–381. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_29
Mammar, A., Frappier, M., Laleau, R.: An event-B model of an automotive adaptive exterior light system. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 351–366. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_28
Milhau, J., Frappier, M., Gervais, F., Laleau, R.: Systematic translation rules from ASTD to event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 245–259. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16265-7_18
Nganyewou Tidjon, L., Frappier, M., Leuschel, M., Mammar, A.: Extended algebraic state-transition diagrams. In: 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 146–155. IEEE Computer Society (2018)
Porres, I., Rauf, I.: Generating class contracts from UML protocol statemachines. In: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation. MoDeVVa 2009, ACM, New York, USA (2009)
Porres, I., Rauf, I.: From nondeterministic UML protocol statemachines to class contracts. In: 2010 Third International Conference on Software Testing, Verification and Validation, pp. 107–116 (2010)
Riviere, P., Singh, N.K., Ameur, Y.A., Dupont, G.: Formalising liveness properties in event-b with the reflexive EB4EB framework. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13903, pp. 312–331. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33170-1_19
Said, M.Y., Butler, M.J., Snook, C.F.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2015)
Sekerinski, E.: Verifying Statecharts with state invariants. In: 13th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 7–14. IEEE Computer Society (2008)
Tidjon, L.N., Frappier, M., Mammar, A.: Intrusion detection using ASTDs. In: Barolli, L., Amato, F., Moscato, F., Enokido, T., Takizawa, M. (eds.) AINA 2020. AISC, vol. 1151, pp. 1397–1411. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44041-1_118
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Cartellier, Q., Frappier, M., Mammar, A. (2023). Proving Local Invariants in ASTDs. In: Li, Y., Tahar, S. (eds) Formal Methods and Software Engineering. ICFEM 2023. Lecture Notes in Computer Science, vol 14308. Springer, Singapore. https://doi.org/10.1007/978-981-99-7584-6_14
Download citation
DOI: https://doi.org/10.1007/978-981-99-7584-6_14
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-7583-9
Online ISBN: 978-981-99-7584-6
eBook Packages: Computer ScienceComputer Science (R0)