{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T03:57:53Z","timestamp":1763179073471,"version":"3.44.0"},"reference-count":79,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"funder":[{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000112344\/14\/NL\/FE"],"award-info":[{"award-number":["4000112344\/14\/NL\/FE"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1016\/j.jss.2018.07.053","type":"journal-article","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T10:01:49Z","timestamp":1532080909000},"page":"52-78","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":31,"special_numbering":"C","title":["Early validation of system requirements and design through correctness-by-construction"],"prefix":"10.1016","volume":"145","author":[{"given":"Emmanouela","family":"Stachtiari","sequence":"first","affiliation":[]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Bliudze","sequence":"additional","affiliation":[]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/j.jss.2018.07.053_bib0001","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1017\/S096012951200028X","article-title":"Rigorous implementation of real-time systems - from theory to application","volume":"23","author":"Abdellatif","year":"2013","journal-title":"Math. Struct. Comput. Sci."},{"year":"2013","key":"10.1016\/j.jss.2018.07.053_bib0002","article-title":"CESAR - Cost-efficient Methods and Processes for Safety-relevant Embedded Systems"},{"key":"10.1016\/j.jss.2018.07.053_bib0004","series-title":"Proc. of the 14th Int. Conf. on Computational Science and Its Applications (ICCSA 2014), Part V","first-page":"370","article-title":"A structured approach for eliciting, modeling, and using quality-related domain knowledge","volume":"vol. 8583","author":"Alebrahim","year":"2014"},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0005","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/258077.258078","article-title":"A formal basis for architectural connection","volume":"6","author":"Allen","year":"1997","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0006","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s00165-015-0349-8","article-title":"A general framework for architecture composability","volume":"28","author":"Attie","year":"2016","journal-title":"Formal Aspects Comput."},{"year":"2008","series-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier","key":"10.1016\/j.jss.2018.07.053_bib0007"},{"year":"1982","series-title":"The Use of Requirements in Rigorous System Design","author":"Baker","key":"10.1016\/j.jss.2018.07.053_bib0008"},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0009","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","article-title":"Rigorous component-based system design using the bip framework","volume":"28","author":"Basu","year":"2011","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2018.07.053_bib0010","series-title":"10th Int. Symp. on Formal Methods for Components and Objects (FMCO 2011)","first-page":"314","article-title":"Component assemblies in the context of manycore","volume":"vol. 7542","author":"Basu","year":"2013"},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0011","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","article-title":"Rigorous component-based system design using the BIP framework","volume":"28","author":"Basu","year":"2011","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2018.07.053_bib0012","series-title":"Proceedings of the 3rd International Conference on NASA Formal Methods","first-page":"453","article-title":"D-Finder 2: towards efficient correctness of incremental design","author":"Bensalem","year":"2011"},{"key":"10.1016\/j.jss.2018.07.053_bib0013","series-title":"Research Report, RR-8759","article-title":"Contracts for Systems Design: Theory","author":"Benveniste","year":"2015"},{"key":"10.1016\/j.jss.2018.07.053_bib0014","series-title":"Computer Aided Verification","first-page":"60","article-title":"Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs","author":"Biere","year":"1999"},{"key":"10.1016\/j.jss.2018.07.053_bib0015","unstructured":"BIPtools, http:\/\/www-verimag.imag.fr\/BIP-Tools,93.html (accessed in 30 July, 2018)."},{"key":"10.1016\/j.jss.2018.07.053_bib0016","series-title":"13th International Symposium on Automated Technology for Verification and Analysis (ATVA \u201915)","first-page":"326","article-title":"Formal verification of infinite-state BIP models","volume":"vol. 9364","author":"Bliudze","year":"2015"},{"key":"10.1016\/j.jss.2018.07.053_bib0017","series-title":"Proceedings of the 17th International ACM Sigsoft Symposium on Component-based Software Engineering","first-page":"169","article-title":"Architecture internalisation in bip","author":"Bliudze","year":"2014"},{"article-title":"Bridging the gap between natural language requirements and formal specifications","year":"2016","author":"B\u00f6schen","key":"10.1016\/j.jss.2018.07.053_bib0018"},{"key":"10.1016\/j.jss.2018.07.053_bib0019","series-title":"Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I","first-page":"518","article-title":"Formal design and safety analysis of air6110 wheel brake system","volume":"vol. 9206","author":"Bozzano","year":"2015"},{"key":"10.1016\/j.jss.2018.07.053_bib0020","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.ress.2014.07.003","article-title":"Spacecraft early design validation using formal methods","volume":"132","author":"Bozzano","year":"2014","journal-title":"Reliab. Eng. Syst. Safety"},{"article-title":"The Engineering Design of Systems: Models and Methods","year":"2016","author":"Buede","key":"10.1016\/j.jss.2018.07.053_bib0021"},{"key":"10.1016\/j.jss.2018.07.053_bib0022","series-title":"Computer Aided Verification","first-page":"334","article-title":"The nuXmv symbolic model checker","volume":"vol. 8559","author":"Cavada","year":"2014"},{"key":"10.1016\/j.jss.2018.07.053_bib0023","series-title":"Computer Aided Verification - 28th International Conference, CAV","first-page":"95","article-title":"Structural synthesis for GXW specifications","author":"Cheng","year":"2016"},{"key":"10.1016\/j.jss.2018.07.053_bib0024","series-title":"2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","first-page":"702","article-title":"Ocra: A tool for checking the refinement of temporal contracts","author":"Cimatti","year":"2013"},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0025","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/1348250.1348253","article-title":"Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning","volume":"17","author":"Cobleigh","year":"2008","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10.1016\/j.jss.2018.07.053_bib0026","series-title":"DATE","first-page":"1023","article-title":"Using contract-based component specifications for virtual integration testing and architecture design.","author":"Damm","year":"2011"},{"key":"10.1016\/j.jss.2018.07.053_bib0027","series-title":"Proc. of the 34th Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2014)","first-page":"284","article-title":"Formal verification of complex properties on PLC programs","author":"Darvas","year":"2014"},{"key":"10.1016\/j.jss.2018.07.053_bib0028","series-title":"Proceedings of the 21st International Conference on Software Engineering","first-page":"411","article-title":"Patterns in property specifications for finite-state verification","author":"Dwyer","year":"1999"},{"key":"10.1016\/j.jss.2018.07.053_bib0029","series-title":"DDECS","first-page":"271","article-title":"Dodt: Increasing requirements formalism using domain ontologies for improved embedded systems development.","author":"Farfeleder","year":"2011"},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0030","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/s00766-004-0191-7","article-title":"Specifying and analyzing early requirements in tropos","volume":"9","author":"Fuxman","year":"2004","journal-title":"Require. Eng."},{"key":"10.1016\/j.jss.2018.07.053_bib0031","series-title":"Proceedings of the 16th International Conference on Software Engineering","first-page":"135","article-title":"On formal requirements modeling languages: Rml revisited","author":"Greenspan","year":"1994"},{"key":"10.1016\/j.jss.2018.07.053_bib0032","series-title":"ECSS-E-ST-10C - System Engineering General Requirements","first-page":"1","author":"Group","year":"2009"},{"key":"10.1016\/j.jss.2018.07.053_bib0033","series-title":"ECSS-M-ST-10C - Space Project management: project planning and implementation","first-page":"1","author":"Group","year":"2009"},{"key":"10.1016\/j.jss.2018.07.053_bib0034","series-title":"Proceedings of the 30th International Conference on Software Engineering","first-page":"31","article-title":"Specification patterns for probabilistic quality properties","author":"Grunske","year":"2008"},{"key":"10.1016\/j.jss.2018.07.053_bib0035","series-title":"Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology","first-page":"83","article-title":"Synchronous observers and the verification of reactive systems","author":"Halbwachs","year":"1994"},{"year":"2010","series-title":"Requirements Engineering","author":"Hull","key":"10.1016\/j.jss.2018.07.053_bib0036"},{"key":"10.1016\/j.jss.2018.07.053_bib0037","series-title":"Infotech@Aerospace 2012, Garden Grove, California, USA, June 19\u201321, 2012","article-title":"A model-based approach to engineering behavior of complex aerospace systems","author":"Ingham","year":"2012"},{"key":"10.1016\/j.jss.2018.07.053_bib0038","series-title":"Engineering Theories of Software Construction (Proceedings of the NATO Summer School","article-title":"Problem analysis and structure","author":"Jackson","year":"2000"},{"key":"10.1016\/j.jss.2018.07.053_bib0039","series-title":"Proceedings of the Fifth International Conference on Quality Software","first-page":"223","article-title":"Ontology based requirements analysis: Lightweight semantic processing approach","author":"Kaiya","year":"2005"},{"year":"2010","series-title":"A Practical Theory of Reactive Systems: Incremental Modeling of Dynamic Behaviors","author":"Kurki-Suonio","key":"10.1016\/j.jss.2018.07.053_bib0040"},{"key":"10.1016\/j.jss.2018.07.053_bib0041","series-title":"Proceedings of the 38th Annual Hawaii International Conference on System Sciences","first-page":"188b","article-title":"Analyzing the quality of domain models developed by novice systems analysts","author":"Leung","year":"2005"},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0042","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1177\/1063293X9600400307","article-title":"A requirement ontology for engineering design","volume":"4","author":"Lin","year":"1996","journal-title":"Concurrent Eng."},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0043","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/52.268955","article-title":"Understanding quality in conceptual modeling","volume":"11","author":"Lindland","year":"1994","journal-title":"IEEE Softw."},{"issue":"4","key":"10.1016\/j.jss.2018.07.053_bib0044","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10009-010-0174-6","article-title":"Toolday: a tool for domain analysis","volume":"13","author":"Lisboa","year":"2011","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.jss.2018.07.053_bib0045","series-title":"NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017, Proceedings","first-page":"427","article-title":"Just formal enough? automated analysis of EARS requirements","author":"L\u00facio","year":"2017"},{"key":"10.1016\/j.jss.2018.07.053_bib0046","series-title":"10th IEEE International Symposium on Industrial Embedded Systems (SIES)","first-page":"1","article-title":"Resa: an ontology-based requirement specification language tailored to automotive systems","author":"Mahmud","year":"2015"},{"key":"10.1016\/j.jss.2018.07.053_bib0047","series-title":"Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Trento, Italy, September 4\u20138, 2017, Proceedings","first-page":"332","article-title":"Specification and semantic analysis of embedded systems requirements: From description logic to temporal logic","volume":"vol. 10469","author":"Mahmud","year":"2017"},{"issue":"6","key":"10.1016\/j.jss.2018.07.053_bib0048","doi-asserted-by":"crossref","first-page":"869","DOI":"10.1109\/TSE.2012.74","article-title":"What industry needs from architectural languages: a survey","volume":"39","author":"Malavolta","year":"2013","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"10.1016\/j.jss.2018.07.053_bib0049","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1109\/52.646889","article-title":"Using viewpoints to define domain requirements","volume":"15","author":"Mannion","year":"1998","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2018.07.053_bib0050","series-title":"RE 2010, 18th IEEE International Requirements Engineering Conference","first-page":"277","article-title":"Big ears (the return of \u201ceasy approach to requirements engineering\u201d)","author":"Mavin","year":"2010"},{"key":"10.1016\/j.jss.2018.07.053_bib0051","series-title":"Proceedings of the 2009 17th IEEE International Requirements Engineering Conference, RE","first-page":"317","article-title":"Easy approach to requirements syntax (ears)","author":"Mavin","year":"2009"},{"key":"10.1016\/j.jss.2018.07.053_bib0052","series-title":"Proceedings 9th Interaction and Concurrency Experience (ICE)","first-page":"83","article-title":"Architecture diagrams: a graphical language for architecture style specification","volume":"vol. 223","author":"Mavridou","year":"2016"},{"issue":"1","key":"10.1016\/j.jss.2018.07.053_bib0053","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.jlamp.2016.05.002","article-title":"Configuration logics: modeling architecture styles","volume":"86","author":"Mavridou","year":"2017","journal-title":"J. Logic. Algebraic Methods Programm."},{"key":"10.1016\/j.jss.2018.07.053_bib0054","series-title":"Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD), EPTCS vol. 272","article-title":"DesignBIP: a design studio for modeling and generating systems with BIP","author":"Mavridou","year":"2018"},{"key":"10.1016\/j.jss.2018.07.053_bib0055","series-title":"Proceedings of the 13th International Conderence of Formal Aspects in Component Software","article-title":"Architecture-based design: a satellite on-board software case study","author":"Mavridou","year":"2016"},{"key":"10.1016\/j.jss.2018.07.053_sbref0055","series-title":"Technical Report, 221156","article-title":"Architecture-Based Design: A Satellite On-Board Software Case Study","author":"Mavridou","year":"2016"},{"issue":"1","key":"10.1016\/j.jss.2018.07.053_bib0057","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/32.825767","article-title":"A classification and comparison framework for software architecture description languages","volume":"26","author":"Medvidovic","year":"2000","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jss.2018.07.053_sbref0003","series-title":"Technical Report","article-title":"Requirements Specification Language and Requirements Meta Model","author":"Mitschke","year":"2010"},{"issue":"4","key":"10.1016\/j.jss.2018.07.053_bib0058","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","article-title":"Proving the shalls: early validation of requirements through formal methods","volume":"8","author":"Miller","year":"2006","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.jss.2018.07.053_bib0059","series-title":"Fourth International Symposium on Software Engineering in Healthcare workshop (SEHC 2014)","article-title":"From requirements to code: model based development of a medical cyber physical system","author":"Murugesan","year":"2014"},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0060","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/2658982.2527272","article-title":"Compositional verification of a medical device system","volume":"33","author":"Murugesan","year":"2013","journal-title":"ACM SIGAda Ada Lett."},{"key":"10.1016\/j.jss.2018.07.053_bib0061","series-title":"11th Int. Symp. on Formal Aspects of Component Software (FACS 2014)","first-page":"288","article-title":"Reduction and abstraction techniques for BIP","author":"Noureddine","year":"2015"},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0062","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s10009-014-0313-6","article-title":"Statistical model checking qos properties of systems with sbip","volume":"17","author":"Nouri","year":"2015","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0063","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1109\/2.910904","article-title":"Weaving together requirements and architectures","volume":"34","author":"Nuseibeh","year":"2001","journal-title":"Computer"},{"key":"10.1016\/j.jss.2018.07.053_bib0064","unstructured":"NXP, 2007. Um10204: I2c-bus specification and user manual."},{"key":"10.1016\/j.jss.2018.07.053_bib0065","series-title":"Engineering of Computer-Based Systems, 2004. Proceedings. 11th IEEE International Conference and Workshop on the","first-page":"44","article-title":"An explicit definition of connectors for component-based software architecture","author":"Oussalah","year":"2004"},{"key":"10.1016\/j.jss.2018.07.053_bib0066","article-title":"On weighted configuration logics","volume":"abs\/1704.04969","author":"Paraponiari","year":"2017","journal-title":"CoRR"},{"key":"10.1016\/j.jss.2018.07.053_bib0067","first-page":"394","article-title":"Rtd-finder: a tool for compositional verification of real-time component-based systems","author":"Rayana","year":"2016"},{"key":"10.1016\/j.jss.2018.07.053_bib0068","series-title":"Software Engineering 2011 - Workshopband (inkl. Doktorandensymposium), Fachtagung des GI-Fachbereichs Softwaretechnik, 21.-25.02.2011, Karlsruhe","first-page":"99","article-title":"A pattern-based requirement specification language: Mapping automotive specific timing requirements","author":"Reinkemeier","year":"2011"},{"key":"10.1016\/j.jss.2018.07.053_bib0069","series-title":"Proceedings of the NAACL HLT 2010 Young Investigators Workshop on Computational Approaches to Languages of the Americas","first-page":"100","article-title":"Automated detection of language issues affecting accuracy, ambiguity and verifiability in software requirements written in natural language","author":"Rojas","year":"2010"},{"key":"10.1016\/j.jss.2018.07.053_bib0070","series-title":"Advances in the Astronautical Sciences","first-page":"1513","article-title":"CubETH magnetotorquers: Design and tests for a CubeSat mission","volume":"vol. 153","author":"Rossi","year":"2015"},{"issue":"4","key":"10.1016\/j.jss.2018.07.053_bib0071","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1561\/1000000034","article-title":"Rigorous system design","volume":"6","author":"Sifakis","year":"2013","journal-title":"Found. Trends Electron. Des. Autom."},{"issue":"7","key":"10.1016\/j.jss.2018.07.053_bib0072","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1145\/358557.358572","article-title":"On the inevitable intertwining of specification and implementation","volume":"25","author":"Swartout","year":"1982","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jss.2018.07.053_bib0073","unstructured":"UML,. Unified modeling language specification, version 2.5.1. http:\/\/www.omg.org\/spec\/UML\/2.5.1\/ (accessed in 30 July, 2018)."},{"issue":"3","key":"10.1016\/j.jss.2018.07.053_bib0074","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1109\/2.825699","article-title":"The koala component model for consumer electronics software","volume":"33","author":"Van Ommering","year":"2000","journal-title":"Computer"},{"key":"10.1016\/j.jss.2018.07.053_bib0075","series-title":"2012 IEEE Aerospace Conference","first-page":"1","article-title":"An ontology for state analysis: Formalizing the mapping to sysml","author":"Wagner","year":"2012"},{"key":"10.1016\/j.jss.2018.07.053_bib0076","series-title":"1st Symp. on Dependable Software Engineering Theories, Tools and Applications (SETTA 2015)","first-page":"277","article-title":"Automatic fault localization for BIP","author":"Wang","year":"2015"},{"issue":"2","key":"10.1016\/j.jss.2018.07.053_bib0077","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MS.2012.173","article-title":"Your \u201cwhat\u201d is my \u201chow\u201d: iteration and hierarchy in system design","volume":"30","author":"Whalen","year":"2013","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2018.07.053_bib0078","series-title":"Software Architecture, 2005. WICSA 2005. 5th Working IEEE\/IFIP Conference on","first-page":"243","article-title":"Architecture description languages in practice session report","author":"Woods","year":"2005"},{"issue":"1","key":"10.1016\/j.jss.2018.07.053_bib0079","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/237432.237434","article-title":"Four dark corners of requirements engineering","volume":"6","author":"Zave","year":"1997","journal-title":"ACM Trans. Softw. Eng. Methodol."}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016412121830150X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016412121830150X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T23:19:12Z","timestamp":1759015152000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016412121830150X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":79,"alternative-id":["S016412121830150X"],"URL":"https:\/\/doi.org\/10.1016\/j.jss.2018.07.053","relation":{},"ISSN":["0164-1212"],"issn-type":[{"type":"print","value":"0164-1212"}],"subject":[],"published":{"date-parts":[[2018,11]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Early validation of system requirements and design through correctness-by-construction","name":"articletitle","label":"Article Title"},{"value":"Journal of Systems and Software","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jss.2018.07.053","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2018 Published by Elsevier Inc.","name":"copyright","label":"Copyright"}]}}