{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:36Z","timestamp":1740107976051,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,6,22]],"date-time":"2021-06-22T00:00:00Z","timestamp":1624320000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,22]],"date-time":"2021-06-22T00:00:00Z","timestamp":1624320000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005722","name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005722","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Full a posteriori verification of the correctness of modern software systems is practically infeasible due to the sheer complexity resulting from their intrinsic concurrent nature. An alternative approach consists of ensuring <jats:italic>correctness by construction<\/jats:italic>. We discuss the <jats:italic>Rigorous System Design<\/jats:italic> (RSD) approach, which relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way. In particular, we highlight some of the key requirements for the feasibility of such an approach, namely availability of (1)\u00a0methods and tools for the design of correct-by-construction high-level models and (2)\u00a0definition and proof of the validity of suitable domain-specific abstractions. We summarise the results of the extended versions of seven papers selected among those presented at the <jats:inline-formula><jats:alternatives><jats:tex-math>$$1\\mathrm {st}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mi>st<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and the <jats:inline-formula><jats:alternatives><jats:tex-math>$$2\\mathrm {nd}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>2<\/mml:mn>\n                    <mml:mi>nd<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u00a0International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018\u20132019), indicating how they contribute to the advancement of the RSD approach.\n<\/jats:p>","DOI":"10.1007\/s10009-021-00632-0","type":"journal-article","created":{"date-parts":[[2021,6,22]],"date-time":"2021-06-22T19:02:27Z","timestamp":1624388547000},"page":"679-684","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On methods and tools for rigorous system design"],"prefix":"10.1007","volume":"23","author":[{"given":"Simon","family":"Bliudze","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Wirsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,22]]},"reference":[{"issue":"2","key":"632_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s00165-015-0349-8","volume":"18","author":"P Attie","year":"2016","unstructured":"Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Formal Aspects Comput. 18(2), 207\u2013231 (2016). https:\/\/doi.org\/10.1007\/s00165-015-0349-8","journal-title":"Formal Aspects Comput."},{"key":"632_CR2","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ni$$\\check{c}$$kovi$$\\acute{c}$$, D.: Automatic failure explanation in CPS models. In: P.C. \u00d6lveczky, G.\u00a0Sala\u00fcn (eds.) Proceedings of the 17th International Conference Software Engineering and Formal Methods (SEFM 2019), Lecture Notes in Computer Science, vol. 11724, pp. 69\u201386. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_4","DOI":"10.1007\/978-3-030-30446-1_4"},{"key":"632_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00599-4","author":"E Bartocci","year":"2021","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Nickovic, D.: CPSDebug: Automatic failure explanation in CPS models. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00599-4","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR4","unstructured":"Bass, L., Clements, P., Kazman, R.: Software Architecture in Practice, 3rd edn. SEI Series in Software Engineering. Addison-Wesley Professional (2012)"},{"key":"632_CR5","doi-asserted-by":"publisher","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: $$4^{th}$$ IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM06), pp. 3\u201312 (2006). https:\/\/doi.org\/10.1109\/SEFM.2006.27. Invited talk","DOI":"10.1109\/SEFM.2006.27"},{"key":"632_CR6","unstructured":"Basu, A., Gallien, M., Lesire, C., Nguyen, T.H., Bensalem, S., Ingrand, F., Sifakis, J.: Incremental component-based construction and verification of a robotic system. In: ECAI, pp. 631\u2013635 (2008)"},{"key":"632_CR7","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.G.: Contracts for system design. Research Report RR-8147, INRIA (2012). https:\/\/hal.inria.fr\/hal-00757488"},{"key":"632_CR8","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: W.J. Fokkink, R.\u00a0van Glabbeek (eds.) 30th International Conference on Concurrency Theory, (CONCUR 2019), LIPIcs, vol. 140, pp. 33:1\u201333:15. Schloss Dagstuhl \u2014 Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.33","DOI":"10.4230\/LIPIcs.CONCUR.2019.33"},{"key":"632_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00603-x","author":"N Bertrand","year":"2021","unstructured":"Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00603-x","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR10","doi-asserted-by":"publisher","unstructured":"Bliudze, S., Bensalem, S. (eds.): Proceedings of the 1st international workshop on methods and tools for rigorous system design, MeTRiD@ETAPS 2018, EPTCS, vol. 272. Thessaloniki, Greece (2018). https:\/\/doi.org\/10.4204\/EPTCS.272","DOI":"10.4204\/EPTCS.272"},{"issue":"3","key":"632_CR11","doi-asserted-by":"publisher","first-page":"1613","DOI":"10.1007\/s10270-017-0642-5","volume":"18","author":"S Bliudze","year":"2019","unstructured":"Bliudze, S., Furic, S., Sifakis, J., Viel, A.: Rigorous design of cyber-physical systems: linking physicality and computation. Int. J. Software Syst. Model. 18(3), 1613\u20131636 (2019). https:\/\/doi.org\/10.1007\/s10270-017-0642-5","journal-title":"Int. J. Software Syst. Model."},{"key":"632_CR12","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"publisher","DOI":"10.2200\/S00658ED1V01Y201508DCT013","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool, California (2015)"},{"key":"632_CR13","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: A.\u00a0Egyed, I.\u00a0Schaefer (eds.) Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015), Lecture Notes in Computer Science, vol. 9033, pp. 202\u2013217. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_14","DOI":"10.1007\/978-3-662-46675-9_14"},{"key":"632_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00601-z","author":"S Blom","year":"2021","unstructured":"Blom, S., Darabi, S., Huisman, M., Safari, M.: Correct program parallelisations. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00601-z","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR15","doi-asserted-by":"publisher","unstructured":"Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs. In: C.W. Barrett, M.\u00a0Davies, T.\u00a0Kahsai (eds.) Proceedings of the 9th NASA Formal Methods International Symposium (NFM 2017), Lecture Notes in Computer Science, vol. 10227, pp. 247\u2013264. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_17","DOI":"10.1007\/978-3-319-57288-8_17"},{"key":"632_CR16","doi-asserted-by":"publisher","unstructured":"El Ballouli, R., Bensalem, S., Bozga, M., Sifakis, J.: Four exercises in programming dynamic reconfigurable systems: Methodology and solution in DR-BIP. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems (ISoLA 2018), Lecture Notes in Computer Science, vol. 11246, pp. 304\u2013320. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_20","DOI":"10.1007\/978-3-030-03424-5_20"},{"key":"632_CR17","doi-asserted-by":"publisher","unstructured":"El Ballouli, R., Bensalem, S., Bozga, M., Sifakis, J.: Programming dynamic reconfigurable systems. In: K.\u00a0Bae, P.C. \u00d6lveczky (eds.) Proceedings of the 15th International Conference Formal Aspects of Component Software (FACS 2018), Lecture Notes in Computer Science, vol. 11222, pp. 118\u2013136. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02146-7_6","DOI":"10.1007\/978-3-030-02146-7_6"},{"key":"632_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00596-7","author":"R El Ballouli","year":"2021","unstructured":"El Ballouli, R., Bensalem, S., Bozga, M., Sifakis, J.: Programming dynamic reconfigurable systems. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00596-7","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR19","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201995, pp. 85\u201394. Association for Computing Machinery, New York, NY, USA (1995). https:\/\/doi.org\/10.1145\/199448.199468","DOI":"10.1145\/199448.199468"},{"key":"632_CR20","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software, 1st edn. Addison-Wesley Professional, Boston (1994)","edition":"1"},{"key":"632_CR21","doi-asserted-by":"publisher","unstructured":"Gouglidis, A., Grompanopoulos, C., Mavridou, A.: Formal verification of usage control models: a case study of UseCON using TLA+. In: S.\u00a0Bliudze, S.\u00a0Bensalem (eds.) Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD), Electronic Proceedings in Theoretical Computer Science, vol. 272, pp. 52\u201364. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/EPTCS.272.5","DOI":"10.4204\/EPTCS.272.5"},{"key":"632_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00600-0","author":"C Grompanopoulos","year":"2021","unstructured":"Grompanopoulos, C., Gouglidis, A., Mavridou, A.: Specifying and verifying usage control models and policies in TLA$${}^+$$. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00600-0","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR23","doi-asserted-by":"publisher","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.: A compositional approach for schedulability analysis of distributed avionics systems. In: S.\u00a0Bliudze, S.\u00a0Bensalem (eds.) Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD), Electronic Proceedings in Theoretical Computer Science, vol. 272, pp. 39\u201351. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/eptcs.272.4","DOI":"10.4204\/eptcs.272.4"},{"key":"632_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00597-6","author":"P Han","year":"2021","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.: Model-based optimization of ARINC-653 partition scheduling. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00597-6","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR25","doi-asserted-by":"publisher","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In: P.\u00a0Baldan, D.\u00a0Gorla (eds.) Proceedings of the 25th International Conference on Concurrency Theory (CONCUR 2014), Lecture Notes in Computer Science, vol. 8704, pp. 125\u2013140. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_10","DOI":"10.1007\/978-3-662-44584-6_10"},{"key":"632_CR26","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"IV Konnov","year":"2017","unstructured":"Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017). https:\/\/doi.org\/10.1016\/j.ic.2016.03.006","journal-title":"Inf. Comput."},{"key":"632_CR27","doi-asserted-by":"publisher","unstructured":"Lekidis, A., Katsaros, P.: Model-based design of energy-efficient applications for iot systems. In: S.\u00a0Bliudze, S.\u00a0Bensalem (eds.) Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD), Electronic Proceedings in Theoretical Computer Science, vol. 272, pp. 24\u201338. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/eptcs.272.3","DOI":"10.4204\/eptcs.272.3"},{"key":"632_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00598-5","author":"A Lekidis","year":"2021","unstructured":"Lekidis, A., Katsaros, P.: Energy characterization of IoT systems through design aspect monitoring. Int. J. Software Tools Technol. Transf. (2021). https:\/\/doi.org\/10.1007\/s10009-020-00598-5","journal-title":"Int. J. Software Tools Technol. Transf."},{"key":"632_CR29","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert \u2013 A formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE, Toulouse, France (2016). https:\/\/hal.inria.fr\/hal-01238879"},{"key":"632_CR30","doi-asserted-by":"publisher","unstructured":"Marmsoler, D.: Hierarchical specification and verification of architectural design patterns. In: A.\u00a0Russo, A.\u00a0Sch\u00fcrr (eds.) Proceedings of the 21st International Conference Fundamental Approaches to Software Engineering (FASE 2018), Lecture Notes in Computer Science, vol. 10802, pp. 149\u2013168. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89363-1_9","DOI":"10.1007\/978-3-319-89363-1_9"},{"key":"632_CR31","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: a satellite on-board software case study. In: 13th International Conference on Formal Aspects of Component Software (FACS 2016), Lecture Notes in Computer Science, vol. 10231, pp. 260\u2013279 (2016). https:\/\/doi.org\/10.1007\/978-3-319-57666-4_16","DOI":"10.1007\/978-3-319-57666-4_16"},{"key":"632_CR32","doi-asserted-by":"publisher","unstructured":"Rosen, R., von Wichert, G., Lo, G., Bettenhausen, K.D.: About the importance of autonomy and digital twins for the future of manufacturing. IFAC-PapersOnLine 48(3), 567\u2013572 (2015). https:\/\/doi.org\/10.1016\/j.ifacol.2015.06.141. 15th IFAC Symposium on Information Control Problems in Manufacturing","DOI":"10.1016\/j.ifacol.2015.06.141"},{"key":"632_CR33","doi-asserted-by":"publisher","unstructured":"Sifakis, J. Rigorous system design. Foundations and $$\\text{Trends}^{\\textregistered }$$ in Electronic Design Automation 6(4), 293\u2013362 (2012) . https:\/\/doi.org\/10.1561\/1000000034","DOI":"10.1561\/1000000034"},{"key":"632_CR34","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jss.2018.07.053","volume":"145","author":"E Stachtiari","year":"2018","unstructured":"Stachtiari, E., Mavridou, A., Katsaros, P., Bliudze, S., Sifakis, J.: Early validation of system requirements and design through correctness-by-construction. J. Syst. Software 145, 52\u201378 (2018). https:\/\/doi.org\/10.1016\/j.jss.2018.07.053","journal-title":"J. Syst. Software"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00632-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00632-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00632-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:06:24Z","timestamp":1637928384000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00632-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,22]]},"references-count":34,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["632"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00632-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2021,6,22]]},"assertion":[{"value":"8 June 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}