@inproceedings{40a7f870e4e64ce39714875d06d928b0,
title = "Capturing System Designs with Formal Executable Specifications",
abstract = "Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.",
keywords = "Executable Specifications, Formal Patterns, Maude, Qualitative and Quantitative Properties, Rewriting Logic, System Design",
author = "Jos{\'e} Meseguer",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 28th International Conference on Fundamental Approaches to Software Engineering, FASE 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025 ; Conference date: 03-05-2025 Through 08-05-2025",
year = "2025",
doi = "10.1007/978-3-031-90900-9\_1",
language = "English (US)",
isbn = "9783031908996",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--32",
editor = "Artur Boronat and Gordon Fraser",
booktitle = "Fundamental Approaches to Software Engineering - 28th International Conference, FASE 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings",
address = "Germany",
}