{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T04:25:00Z","timestamp":1649132700615},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,3,24]],"date-time":"2015-03-24T00:00:00Z","timestamp":1427155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11334-015-0244-8","type":"journal-article","created":{"date-parts":[[2015,3,23]],"date-time":"2015-03-23T03:23:48Z","timestamp":1427081028000},"page":"143-152","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Early detection of evolving system failures and temporal conflicts using parameterized formal specifications and bounded constraint-solving"],"prefix":"10.1007","volume":"11","author":[{"given":"Doron","family":"Drusinsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,3,24]]},"reference":[{"key":"244_CR1","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, Browne A, Chang E, Col\u00f3n M, Kapur A, Manna Z, Sipma HB, Uribe TE (1996) STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In: Proceedings of 8th International Conference Computer Aided Verification, LNCS 1102. Springer, pp 415\u2013418","DOI":"10.1007\/3-540-61474-5_92"},{"key":"244_CR2","doi-asserted-by":"crossref","unstructured":"Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: A Model-Checking Tool for Real-Time Systems. In: Hu AJ, Vardi MY (eds) Proceedings of 10th Internationla Conference Computer-Aided Verification, LNCS 1427. Springer, pp 546\u2013550","DOI":"10.1007\/BFb0055357"},{"key":"244_CR3","doi-asserted-by":"crossref","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1990) Symbolic Model Checking: 10 $$^{20}$$ 20 States and Beyond. In: Proceedings of 5th Annual Symposium on Logic in Computer Science, June 1990","DOI":"10.1109\/LICS.1990.113767"},{"key":"244_CR4","unstructured":"Clarke EM, Emerson EA (1981) Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Kozen D (ed) Proceedings of Workshop on Logic of Programs, LNCS 131. Springer, pp 52\u201371"},{"key":"244_CR5","unstructured":"Drusinsky D (2000) The Temporal Rover and the ATG Rover. In: Proceedings of SPIN, (2000) Workshop, LNCS 1885. Springer, pp 323\u2013329"},{"key":"244_CR6","doi-asserted-by":"crossref","unstructured":"Drusinsky D (2006) Modeling and Verification Using UML Statecharts\u2014A Working Guide to Reactive System Design. Elsevier, Runtime Monitoring and Execution-based Model Checking","DOI":"10.1016\/B978-075067949-7\/50004-0"},{"key":"244_CR7","unstructured":"Drusinsky D (2011) Practical UML-based Specification, Validation, and Verification of Mission-critical Software. Space Exploration and Defense Software Examples in Practice. ISBN: 978-145750-494-5, Dog-Ear Publishing"},{"key":"244_CR8","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/s11334-014-0235-1","volume":"10","author":"D Drusinsky","year":"2014","unstructured":"Drusinsky D (2014) Computer-aided discovery of formal specification behavioral requirements and requirement to implementation mappings. Innovations Syst Softw Eng 10:271\u2013281. doi: 10.1007\/s11334-014-0235-1","journal-title":"Innovations Syst Softw Eng"},{"issue":"4","key":"244_CR9","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1109\/JSYST.2008.2009190","volume":"2","author":"D Drusinsky","year":"2008","unstructured":"Drusinsky D, Michael JB, Shing M (2008) A visual tradeoff space for formal verification and validation techniques. IEEE Syst J 2(4):513\u2013519","journal-title":"IEEE Syst J"},{"key":"244_CR10","doi-asserted-by":"crossref","unstructured":"Drusinsky D, Shing M (2010) Validating Quality Attribute Requirements via Execution-based Model Checking. In: Proceedings of 21st IEEE International Symposium on Rapid Systems Prototyping, George Mason University, Fairfax, VA, 8\u201311 June","DOI":"10.1109\/RSP.2010.5656438"},{"key":"244_CR11","doi-asserted-by":"crossref","unstructured":"Drusinsky D, Michael JB, Otani T, Shing M (2008) Validating UML Statechart-Based Assertions Libraries for Improved Reliability and Assurance. In: Proceedings of 2nd International Conference on Secure System Integration and Reliability Improvement, Yokohama, Japan, 14\u201317 July, pp 47\u201351","DOI":"10.1109\/SSIRI.2008.54"},{"key":"244_CR12","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","unstructured":"Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge"},{"issue":"3","key":"244_CR13","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231\u2013274","journal-title":"Sci Comput Program"},{"issue":"4","key":"244_CR14","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund K, Pressburger T (2000) Model Checking Java Programs using Java PathFinder. Int J Softw Tools Technol Transf 2(4):366\u2013381","journal-title":"Int J Softw Tools Technol Transf"},{"key":"244_CR15","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2004) An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design, vol 24. Springer, Netherlands, pp 189\u2013215","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"issue":"5","key":"244_CR16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann G (1997) The Model Checker SPIN. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"244_CR17","unstructured":"Hopcroft JE, Ullman JD (2006) Introduction to automata theory, languages, and computation. Addison Wesley"},{"key":"244_CR18","doi-asserted-by":"crossref","unstructured":"Nitsche U (1994) Propositional Linear Temporal Logic and Language Homomorphisms. In: Proceedings of 3rd International Symposium on Logical Foundations Computer Science, LNCS 813. Springer, pp 265\u2013277","DOI":"10.1007\/3-540-58140-5_26"},{"key":"244_CR19","unstructured":"Kodkod, A Constraint Solver for Relational Logic, http:\/\/alloy.mit.edu\/kodkod\/"},{"issue":"1\u20132","key":"244_CR20","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a Nutshell. Int J Softw Tools Technol Transf 1(1\u20132):134\u2013152","journal-title":"Int J Softw Tools Technol Transf"},{"key":"244_CR21","doi-asserted-by":"crossref","unstructured":"Meiera A, Mundhenkb M, Thomasa M, Vollmera H (2008) The Complexity of Satisfiability for Fragments of CTL and CTL*Electronic Notes in Theoretical Computer Science, vol 223, 26 December 2008, pp 201\u2013213","DOI":"10.1016\/j.entcs.2008.12.040"},{"key":"244_CR22","unstructured":"NuSMV: a new symbolic model checker, http:\/\/nusmv.fbk.eu\/"},{"key":"244_CR23","doi-asserted-by":"crossref","unstructured":"Paulson LC (1994) Isabelle: A Generic Theorem Prover, LNCS 828. Springer","DOI":"10.1007\/BFb0030541"},{"key":"244_CR24","doi-asserted-by":"crossref","unstructured":"Sammapun U, Lee I, Sokolsky O (2005) RT-MaC: Runtime Monitoring and Checking of Quantitative and Probabilistic Properties. In: Proceedings of 11th IEEE International Conference Embedded and Real-Time Computing Systems and Applications, pp 147\u2013153","DOI":"10.1109\/RTCSA.2005.84"},{"key":"244_CR25","doi-asserted-by":"crossref","unstructured":"Zhang L, Malik S (2002) The Quest for Efficient Boolean Satisfiability Solvers. In: Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July, pp 17\u201336","DOI":"10.1007\/3-540-45657-0_2"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0244-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-015-0244-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-015-0244-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T03:26:37Z","timestamp":1566444397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-015-0244-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,24]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["244"],"URL":"https:\/\/doi.org\/10.1007\/s11334-015-0244-8","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,24]]}}}