×

Towards leveraging domain knowledge in state-based formal methods. (English) Zbl 07495050

Raschke, Alexander (ed.) et al., Logic, computation and rigorous methods. Essays dedicated to Egon Börger on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12750, 1-13 (2021).
Summary: System engineering development processes rely on modelling activities that lead to different design models corresponding to different analyses of the system under consideration.
For the entire collection see [Zbl 1482.68038].

MSC:

68-XX Computer science
03-XX Mathematical logic and foundations

Software:

ProB; Rodin; Z
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial, J.R.: Modeling in Event-B-System and Software Engineering. Cambridge University Press (2010) · Zbl 1213.68214
[2] Aït Ameur, Y.; Baron, M.; Bellatreche, L.; Jean, S.; Sardet, E., Ontologies in engineering: the OntoDB/OntoQL platform, Soft Comput., 21, 2, 369-389 (2017) · doi:10.1007/s00500-015-1633-5
[3] Aït Ameur, Y.; Méry, D., Making explicit domain knowledge in formal system development, Sci. Comput. Program., 121, 100-127 (2016) · doi:10.1016/j.scico.2015.12.004
[4] Ait-Ameur, Y.; Nakajima, S.; Méry, D., Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems (2021), Singapore: Springer, Singapore · doi:10.1007/978-981-15-5054-6
[5] Bjørner, D.: Software Engineering 3 - Domains, Requirements, and Software Design. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2006). doi:10.1007/3-540-33653-2 · Zbl 1095.68022
[6] Bjørner, D., Manifest domains: analysis and description, Formal Asp. Comput., 29, 2, 175-225 (2017) · Zbl 1358.68052 · doi:10.1007/s00165-016-0385-z
[7] Bjørner, D.: Domain analysis and description principles, techniques, and modelling languages. ACM Trans. Softw. Eng. Methodol. 28(2), 8:1-8:67 (2019)
[8] Börger, E., Stärk, R.F.: Abstract State Machines, A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). doi:10.1007/978-3-642-18216-7 · Zbl 1040.68042
[9] Chebieb, A.; Aït Ameur, Y., A formal model for plastic human computer interfaces, Front. Comput. Sci., 12, 2, 351-375 (2018) · doi:10.1007/s11704-016-5460-3
[10] Critical Systems Labs Inc: Nose Gear (NG) Velocity Example Version 1.1, September 2011. http://www.cl.cam.ac.uk/ mjcg/FMStandardsWorkshop/example.pdf
[11] George, C.; Prehn, S.; Toetenel, H., The RAISE specification language a tutorial, VDM ’91 Formal Software Development Methods, 238-319 (1991), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0019998
[12] Gruber, T.R.: Towards principles for the design of ontologies used for knowledge sharing. In: Guarino, N., Poli, R. (eds.) Formal Ontology in Conceptual Analysis and Knowledge Representation. Kluwer Academic Publisher’s, Boston (1993)
[13] Hacid, K., Aït Ameur, Y.: Handling domain knowledge in design and analysis of engineering models. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 74, 1-21 (2017)
[14] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[15] Jackson, M., Zave, P.: Domain descriptions. In: Proceedings of IEEE International Symposium on Requirements Engineering, RE 1993, San Diego, California, USA, 4-6 January 1993, pp. 56-64. IEEE (1993)
[16] Jackson, M.A.: Software Requirements and Specifications - A Lexicon of Practice, Principles and Prejudices. Addison-Wesley, New York (1995)
[17] Mossakowski, T.; James, P.; Roggenbach, M., The distributed ontology, model and specification language - DOL, Recent Trends in Algebraic Development Techniques, 5-10 (2017), Cham: Springer, Cham · Zbl 07152399 · doi:10.1007/978-3-319-72044-9_2
[18] Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1986) · Zbl 0584.68008
[19] Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
[20] van Lamsweerde, A.: Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, New York (2009)
[21] Leuschel, M.; Butler, MJ, ProB: an automated analysis toolset for the B method, Int. J. Softw. Tools Technol. Transf., 10, 2, 185-203 (2008) · doi:10.1007/s10009-007-0063-9
[22] Méry, D.; Sawant, R.; Tarasyuk, A.; Bellatreche, L.; Manolopoulos, Y., Integrating domain-based features into Event-B: A nose gear velocity case study, Model and Data Engineering, 89-102 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-23781-7_8
[23] Mossakowski, T.; Codescu, M.; Neuhaus, F.; Kutz, O.; Koslow, A.; Buchsbaum, A., The distributed ontology, modeling and specification language - DOL, The Road to Universal Logic, 489-520 (2015), Cham: Springer, Cham · Zbl 1409.68284 · doi:10.1007/978-3-319-15368-1_21
[24] Singh, N.K., Aït Ameur, Y., Méry, D.: Formal ontology driven model refactoring. In: 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, pp. 136-145. IEEE Computer Society (2018)
[25] Spivey, J.M.: Z Notation - a Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
[26] Yu, E.S.K.: Towards modeling and reasoning support for early-phase requirements engineering. In: 3rd IEEE International Symposium on Requirements Engineering (RE 1997), 5-8 January 1997. Annapolis, MD, USA, pp. 226-235. IEEE Computer Society (1997)
[27] Zave, P.; Jackson, M., Four dark corners of requirements engineering, ACM Trans. Softw. Eng. Methodol., 6, 1, 1-30 (1997) · doi:10.1145/237432.237434
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.