{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T05:54:54Z","timestamp":1772517294541,"version":"3.50.1"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T00:00:00Z","timestamp":1747094400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T00:00:00Z","timestamp":1747094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10270-025-01291-4","type":"journal-article","created":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T01:06:50Z","timestamp":1747098410000},"page":"271-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Correct-by-construction requirement decomposition"],"prefix":"10.1007","volume":"25","author":[{"given":"Minghui","family":"Sun","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4992-0193","authenticated-orcid":false,"given":"Georgios","family":"Bakirtzis","sequence":"additional","affiliation":[]},{"given":"Hassan","family":"Jafarzadeh","sequence":"additional","affiliation":[]},{"given":"Cody","family":"Fleming","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,13]]},"reference":[{"key":"1291_CR1","unstructured":"Abbasipour, M.: A framework for requirements decomposition, SLA management and dynamic system reconfiguration. PhD thesis, Concordia University (2018)"},{"key":"1291_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-010-0145-Y","author":"J Abrial","year":"2010","unstructured":"Abrial, J., Butler, M.J., Hallerstede, S., et al.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. (2010). https:\/\/doi.org\/10.1007\/S10009-010-0145-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1291_CR3","doi-asserted-by":"crossref","unstructured":"Althoff, M.: An introduction to CORA 2015. In: ARC (2015). https:\/\/doi.org\/10.29007\/zbkv","DOI":"10.29007\/zbkv"},{"key":"1291_CR4","unstructured":"ANSI, EIA 632: Processes for Engineering a System. Electronic Industries Alliance Standard (2003)"},{"key":"1291_CR5","doi-asserted-by":"crossref","unstructured":"Arora, C, Sabetzadeh, M., Briand, L.C., et\u00a0al.: Requirement boilerplates: Transition from manually-enforced to automatically-verifiable natural language patterns. In: RePa (2014). https:\/\/doi.org\/10.1109\/REPA.2014.6894837","DOI":"10.1109\/RePa.2014.6894837"},{"key":"1291_CR6","unstructured":"ARP4754B: Guidelines for development of civil aircraft and systems. Tech. rep. SAE (2023)"},{"key":"1291_CR7","volume-title":"Feedback Systems: An Introduction for Scientists and Engineers","author":"KJ Astr\u00f6m","year":"2010","unstructured":"Astr\u00f6m, K.J., Murray, R.M.: Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, Princeton (2010)"},{"key":"1291_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1291_CR9","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., et al.: Contracts for system design. Foundations and Trends in Electronic Design Automation (2012). https:\/\/doi.org\/10.1561\/1000000053","DOI":"10.1561\/1000000053"},{"key":"1291_CR10","unstructured":"Benveniste, A., Damm, W., Sangiovanni-Vincentelli, A., et al.: Contracts for the design of embedded systems part I: Methodology and use cases. Tech. rep, Inria (2012)"},{"key":"1291_CR11","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., et al.: Contracts for systems design: methodology and application cases. Tech. rep, Inria (2015)"},{"key":"1291_CR12","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., et\u00a0al.: Contracts for systems design: Theory. Foundations and Trends \u00aein Electronic Design Automation (2015b). https:\/\/doi.org\/10.1561\/1000000053","DOI":"10.1561\/1000000053"},{"key":"1291_CR13","doi-asserted-by":"crossref","unstructured":"Benvenuti, L., Ferrari, A., Mangeruca, L., et\u00a0al.: A contract-based formalism for the specification of heterogeneous systems. In: FDL (2008). https:\/\/doi.org\/10.1109\/FDL.2008.4641436","DOI":"10.1109\/FDL.2008.4641436"},{"key":"1291_CR14","doi-asserted-by":"crossref","unstructured":"Blom, H., Chen, D., Kaijser, H., et\u00a0al.: EAST-ADL: an architecture description language for automotive software-intensive systems in the light of recent use and research (2016). https:\/\/doi.org\/10.4018\/IJSDA.2016070101","DOI":"10.4018\/IJSDA.2016070101"},{"key":"1291_CR15","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Katoen, J., et\u00a0al.: A model checker for AADL. In: CAV (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_48","DOI":"10.1007\/978-3-642-14295-6_48"},{"key":"1291_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/S00450-010-0136-Y","author":"P Braun","year":"2014","unstructured":"Braun, P., Broy, M., Houdek, F., et al.: Guiding requirements engineering for software-intensive embedded systems in the automotive industry. Comput. Sci. Res. (2014). https:\/\/doi.org\/10.1007\/S00450-010-0136-Y","journal-title":"Comput. Sci. Res."},{"key":"1291_CR17","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems (2007)"},{"key":"1291_CR18","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: Cortellessa, V., Muccini, H., Demir\u00f6rs, O. (eds.), SEAA (2012). https:\/\/doi.org\/10.1109\/SEAA.2012.68","DOI":"10.1109\/SEAA.2012.68"},{"key":"1291_CR19","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693137","DOI":"10.1109\/ASE.2013.6693137"},{"key":"1291_CR20","doi-asserted-by":"crossref","unstructured":"Cofer, D.D., Gacek, A., Miller, S.P., et\u00a0al.: Compositional verification of architectural models. In: NFM (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13","DOI":"10.1007\/978-3-642-28891-3_13"},{"key":"1291_CR21","doi-asserted-by":"crossref","unstructured":"Damm, W., Hungar, H., Josko, B., et\u00a0al.: Using contract-based component specifications for virtual integration testing and architecture design. In: DAT (2011). https:\/\/doi.org\/10.1109\/DATE.2011.5763167","DOI":"10.1109\/DATE.2011.5763167"},{"key":"1291_CR22","doi-asserted-by":"crossref","unstructured":"dos Santos, C.A.R., Saleh, A.H., Schrijvers, T., et\u00a0al.: CONDEnSe: contract based design synthesis. In: MODELS. IEEE (2019). https:\/\/doi.org\/10.1109\/MODELS.2019.00009","DOI":"10.1109\/MODELS.2019.00009"},{"key":"1291_CR23","unstructured":"DOT\/FAA\/AR-08\/32: Requirements engineering management handbook. Tech. rep., U.S. Department of Transportation Federal Aviation Administration (2009)"},{"key":"1291_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/S10270-015-0481-1","author":"I Dragomir","year":"2017","unstructured":"Dragomir, I., Ober, I., Percebois, C.: Contract-based modeling and verification of timed safety requirements within SysML. Softw. Syst. Mod. (2017). https:\/\/doi.org\/10.1007\/S10270-015-0481-1","journal-title":"Softw. Syst. Mod."},{"key":"1291_CR25","doi-asserted-by":"crossref","unstructured":"Feiler, P.H., Gluch, D.P., Hudak, J.J.: The architecture analysis & design language (AADL): An introduction. Tech. rep, CMU Software Engineering Institute (2006)","DOI":"10.21236\/ADA455842"},{"key":"1291_CR26","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2834926","author":"I Filippidis","year":"2018","unstructured":"Filippidis, I., Murray, R.M.: Layering assume-guarantee contracts for hierarchical system design. Proc. IEE (2018). https:\/\/doi.org\/10.1109\/JPROC.2018.2834926","journal-title":"Proc. IEE"},{"key":"1291_CR27","doi-asserted-by":"crossref","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., et\u00a0al.: SpaceEx: scalable verification of hybrid systems. In: CAV, Lecture Notes in Computer Science (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"1291_CR28","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., et\u00a0al.: FDR3\u2014a modern refinement checker for CSP. In: TACAS (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"1291_CR29","unstructured":"Greising, D., Johnsson, J.: Behind Boeing\u2019s 787 delays. Chicago Tribune (2007). https:\/\/web.archive.org\/web\/20231224040320\/https:\/\/www.buffalo.edu\/content\/dam\/www\/news\/imported\/pdf\/December07\/ChicagoTribPritchardBoeing.pdf"},{"key":"1291_CR30","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Minea, M., Prabhu, V.: Assume-guarantee reasoning for hierarchical hybrid systems. In: HSCC, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_24","DOI":"10.1007\/3-540-45351-2_24"},{"issue":"1145\/509705","key":"1291_CR31","volume":"10","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K., et al.: An assume-guarantee rule for checking simulation. ACM Trans. Program. Lang. S 10(1145\/509705), 509707 (2002)","journal-title":"ACM Trans. Program. Lang. S"},{"key":"1291_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/J.SYSARC.2015.02.003","author":"K Hu","year":"2015","unstructured":"Hu, K., Zhang, T., Yang, Z., et al.: Exploring AADL verification tool through model transformation. J. Syst. Arch. (2015). https:\/\/doi.org\/10.1016\/J.SYSARC.2015.02.003","journal-title":"J. Syst. Arch."},{"key":"1291_CR33","unstructured":"Iber, J., H\u00f6ller, A., Rauter, T., et\u00a0al.: Towards a generic modeling language for contract-based design. In: ModComp@MoDELS (2015). https:\/\/ceur-ws.org\/Vol-1463\/paper4.pdf"},{"key":"1291_CR34","unstructured":"IEEE\/ISO\/IEC 29148-2018: Systems and software engineering\u2014life cycle processes\u2014requirements engineering. Standard, C\/S2ESC (2018)"},{"key":"1291_CR35","doi-asserted-by":"crossref","unstructured":"Johnsen, A., Lundqvist, K., Pettersson, P., et\u00a0al.: Automated verification of aadl-specifications using UPPAAL. In: HASE (2012). https:\/\/doi.org\/10.1109\/HASE.2012.22","DOI":"10.1109\/HASE.2012.22"},{"key":"1291_CR36","doi-asserted-by":"crossref","unstructured":"Jolliffe, G.: Cost-efficient methods and processes for safety relevant embedded systems (CESAR)\u2014an objective overview. In: SS (2010). https:\/\/doi.org\/10.1007\/978-1-84996-086-1_3","DOI":"10.1007\/978-1-84996-086-1_3"},{"key":"1291_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/BF02919970","author":"DP Kirkman","year":"1998","unstructured":"Kirkman, D.P.: Requirement decomposition and traceability. Requir. Eng. (1998). https:\/\/doi.org\/10.1007\/BF02919970","journal-title":"Requir. Eng."},{"key":"1291_CR38","unstructured":"Komoto, H., Tomiyama, T.: A theory of decomposition in system architecting. In: ICED (2011)"},{"issue":"1115\/1","key":"1291_CR39","first-page":"2836453","volume":"10","author":"A Kusiak","year":"1995","unstructured":"Kusiak, A., Larson, N.: Decomposition and representation methods in mechanical design. J. Mech. D 10(1115\/1), 2836453 (1995)","journal-title":"J. Mech. D"},{"key":"1291_CR40","doi-asserted-by":"crossref","unstructured":"Le\u00a0Lann, G.: An analysis of the Ariane 5 flight 501 failure\u2014a system engineering perspective. In: International Conference and Workshop on Engineering of Computer-Based System (1997). https:\/\/doi.org\/10.1109\/ECBS.1997.581900","DOI":"10.1109\/ECBS.1997.581900"},{"key":"1291_CR41","unstructured":"Mahendra, P., Ghazarian, A.: Patterns in the requirements engineering: a survey and analysis study. WSEAS Transaction on Information Science and Application (2014)"},{"key":"1291_CR42","doi-asserted-by":"crossref","unstructured":"Mavin, A., Wilkinson, P., Harwood, A.R.G., et\u00a0al.: Easy approach to requirements syntax (EARS). In: RE (2009). https:\/\/doi.org\/10.1109\/RE.2009.9","DOI":"10.1109\/RE.2009.9"},{"key":"1291_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Correct Hardware Design and Verification Method (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_30","DOI":"10.1007\/3-540-48153-2_30"},{"key":"1291_CR44","unstructured":"Melancon, P.W.: Categorization and representation of functional decomposition by experts. Tech. rep, Naval Postgraduate School (2008)"},{"key":"1291_CR45","volume-title":"Theory of Hierarchical, Multilevel, Systems","author":"MD Mesarovic","year":"2000","unstructured":"Mesarovic, M.D., Macko, D., Takahara, Y.: Theory of Hierarchical, Multilevel, Systems. Elsevier, Amsterdam (2000)"},{"issue":"1109\/32","key":"1291_CR46","first-page":"58782","volume":"10","author":"AP Moore","year":"1990","unstructured":"Moore, A.P.: The specification and verified decomposition of system requirements using CSP. IEEE Trans. Softw. 10(1109\/32), 58782 (1990)","journal-title":"IEEE Trans. Softw."},{"key":"1291_CR47","unstructured":"National Aeronautics and Space Administration, Space Science Library: NASA Systems Engineering Handbook. CreateSpace Independent Publishing Platform (2010)"},{"key":"1291_CR48","doi-asserted-by":"publisher","DOI":"10.1145\/3243216","author":"P Nuzzo","year":"2019","unstructured":"Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., et al.: Stochastic assume-guarantee contracts for cyber-physical system design. ACM Trans. Embed Comput. Syst. (2019). https:\/\/doi.org\/10.1145\/3243216","journal-title":"ACM Trans. Embed Comput. Syst."},{"key":"1291_CR49","unstructured":"Ouimet, M., Lundqvist, K.: Formal software verification: model checking and theorem proving. Tech. rep, MIT (2007)"},{"key":"1291_CR50","unstructured":"Penzenstadler, B.: DeSyRe-decomposition of systems and their requirements. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2011)"},{"key":"1291_CR51","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2011-416","author":"J Raclet","year":"2011","unstructured":"Raclet, J., Badouel, \u00c9., Benveniste, A., et al.: A modal interface theory for component-based design. Fundam. Informat. (2011). https:\/\/doi.org\/10.3233\/FI-2011-416","journal-title":"Fundam. Informat."},{"key":"1291_CR52","unstructured":"Reinkemeier, P., Stierand, I., Rehkop, P., et\u00a0al.: A pattern-based requirement specification language: mapping automotive specific timing requirements. In: SE Workshopband (2011)"},{"key":"1291_CR53","unstructured":"Salter, K.G.: A methodology for decomposing system requirements into data processing requirements. In: ICSE (1976)"},{"key":"1291_CR54","doi-asserted-by":"crossref","unstructured":"Sangiovanni-Vincentelli, A.L., Damm, W., Passerone, R.: Taming Dr. Contract-based design for cyber-physical systems. Eur. J. Contr. Frankenstein (2012). https:\/\/doi.org\/10.3166\/EJC.18.217-238","DOI":"10.3166\/ejc.18.217-238"},{"key":"1291_CR55","unstructured":"Sidky, A.S., Sud, R.R., Bhatia, S., et al.: Problem identification and decomposition within the requirements generation process. Tech. rep, Virginia Tech (2002)"},{"key":"1291_CR56","doi-asserted-by":"publisher","DOI":"10.1145\/3306607","author":"S Wagner","year":"2019","unstructured":"Wagner, S., Fern\u00e1ndez, D.M., Felderer, M., et al.: Status quo in requirements engineering: a theory and a global family of surveys. ACM Trans. Softw. Eng. Method (2019). https:\/\/doi.org\/10.1145\/3306607","journal-title":"ACM Trans. Softw. Eng. Method"},{"key":"1291_CR57","doi-asserted-by":"crossref","unstructured":"Ye, K., Foster, S., Woodcock, J.: Compositional assume-guarantee reasoning of control law diagrams using UTP. In: Emergence, Complexity and Computatio (2020). https:\/\/doi.org\/10.1007\/978-3-030-15792-0_10","DOI":"10.1007\/978-3-030-15792-0_10"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01291-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01291-4","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01291-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T05:00:53Z","timestamp":1772514053000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01291-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,13]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["1291"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01291-4","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,13]]},"assertion":[{"value":"3 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 March 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}