×

zbMATH — the first resource for mathematics

Hybrid specification of reactive systems: an institutional approach. (English) Zbl 1350.68190
Barthe, Gilles (ed.) et al., Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24689-0/pbk). Lecture Notes in Computer Science 7041, 269-285 (2011).
Summary: This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the corresponding functionality. Specifications are given in an expressive variant of hybrid logic which is, at a later stage, translated into first-order logic to bring into scene suitable tool support. The paper’s main contribution is to provide rigorous foundations for the method, framing specification logics as institutions and the translation process as a comorphism between them.
For the entire collection see [Zbl 1225.68009].

MSC:
68Q65 Abstract data types; algebraic specification
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Areces, C., Heguiabehere, J.: Hylores: A hybrid logic prover based on direct resolution. In: Proceedings of Advances in Modal Logic, AiML 2002 (2002) · Zbl 1072.68560
[2] Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of IGPL 8(3), 339–365 (2000) · Zbl 0956.03025
[3] Börger, E., Stärk, R.: Abstract state machines: A method for high-level system design and analysis. Springer, Heidelberg (2003) · Zbl 1040.68042
[4] Diaconescu, R.: Institution-independent Model Theory. Birkhäuser, Basel (2008) · Zbl 1144.03001
[5] Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theor. Comput. Sci. 285(2), 289–318 (2002) · Zbl 1001.68079
[6] Franceschet, M., de Rijke, M.: Model checking for hybrid logics (with an application to semistructured data). Journal of Applied Logic 4(3), 279–304 (2006) · Zbl 1100.68065
[7] Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39, 95–146 (1992) · Zbl 0799.68134
[8] Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: A tableau prover for hybrid logic. Electr. Notes Theor. Comput. Sci. 262, 127–139 (2010) · Zbl 06609670
[9] Heitmeyer, C.L., Kirby, J., Labaw, B.G.: The SCR Method for Formally Specifying, Verifying, and Validating Requirements: Tool Support. In: ICSE, pp. 610–611 (1997)
[10] Hoareau, C., Satoh, I.: Hybrid logics and model checking: A recipe for query processing in location-aware environments. In: AINA, pp. 130–137. IEEE Computer Society, Los Alamitos (2008)
[11] Hoffmann, G., Areces, C.: Htab: a terminating tableaux system for hybrid logic. Electr. Notes Theor. Comput. Sci. 231, 3–19 (2009) · Zbl 1347.68301
[12] Lange, M.: Model checking for hybrid logic. J. of Logic, Lang. and Inf. 18(4), 465–491 (2009) · Zbl 1193.03053
[13] Madeira, A., Faria, J.M., Martins, M.A., Barbosa, L.S.: Hybrid specification of reactive systems: An institutional approach (extended version). Technical Report CCTC-11-03, University of Minho (July 2011) · Zbl 1350.68190
[14] Martins, M.A., Madeira, A., Barbosa, L.S.: Refinement by interpretation in a general setting. Electron. Notes Theor. Comput. Sci. 259, 105–121 (2009) · Zbl 1342.68091
[15] Martins, M.A., Madeira, A., Barbosa, L.S.: Refinement via interpretation. In: Hung, D.V., Krishnan, P. (eds.) SEFM, pp. 250–259. IEEE Computer Society (2009)
[16] Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 283–297. Springer, Heidelberg (2011) · Zbl 1343.03052
[17] Mossakowski, T.: Foundations of heterogeneous specification. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 359–375. Springer, Heidelberg (2003) · Zbl 1278.68208
[18] Mossakowski, T., Haxthausen, A., Sannella, D., Tarlecki, A.: CASL: The common algebraic specification language: Semantics and proof theory. Computing and Informatics 22, 285–321 (2003) · Zbl 1104.68365
[19] Mossakowski, T., Maeder, C., Codescu, M., Lucke, D.: Hets user guide - version 0.97. Technical report, DFKI Lab Bremen (March 2011), http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/index_e.htm
[20] Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007) · Zbl 05185799
[21] Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. Electron. Notes Theor. Comput. Sci. 174, 63–77 (2007) · Zbl 1278.03048
[22] Rodrigues, C.J., Martins, M.A., Madeira, A., Barbosa, L.S.: Refinement by interpretation in {\(\pi\)}-institutions. EPTCS 55, 53–64 (2011)
[23] Sannella, D.: Algebraic specification and program development by stepwise refinement (Extended abstract). In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 1–9. Springer, Heidelberg (2000) · Zbl 0964.68564
[24] Tarlecki, A.: Abstract specification theory: An overview. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logics of Engineering Software. NATO Science Series, Computer and Systems Sciences, vol. 191, pp. 43–79. IOS Press, Amsterdam (2003)
[25] van Eijck, J.: Hylotab-tableau-based theorem proving for hybrid logics. Technical report, CWI (2002), http://homepages.cwi.nl/ jve/#Publications
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.