{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T09:04:08Z","timestamp":1743498248585},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2012,7,6]],"date-time":"2012-07-06T00:00:00Z","timestamp":1341532800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1007\/s10009-012-0238-x","type":"journal-article","created":{"date-parts":[[2012,7,5]],"date-time":"2012-07-05T19:45:04Z","timestamp":1341517504000},"page":"673-702","source":"Crossref","is-referenced-by-count":8,"title":["Constructive model-based analysis for safety assessment"],"prefix":"10.1007","volume":"14","author":[{"given":"Adriano","family":"Gomes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Mota","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felipe","family":"Ferri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edson","family":"Watanabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,7,6]]},"reference":[{"key":"238_CR1","unstructured":"Haasl, D., Roberts, N., Vesely, W., Goldberg, F. Fault Tree Handbook. Fault Tree Handbook, Systems and Reliability Research, vol. 88. Office of Nuclear Regulatory, US Nuclear Regulatory Commission Research (1981)"},{"key":"238_CR2","unstructured":"ARP4754: Certification Considerations for Highly-Integrated or Complex Aircraft Systems. Aerospace Recommended Practice (SAE International). Warrendale, PA (December 1994)"},{"key":"238_CR3","unstructured":"ARP4761: Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems. Aerospace Recommended Practice (SAE International). Warrendale, PA (December 1996)"},{"key":"238_CR4","unstructured":"FAR25.1309: Federal Aviation Regulations FAR Part 25.1309: System Design and Analysis. Advisory Circular (FAA, USA) (1977)"},{"key":"238_CR5","first-page":"38","volume-title":"Markovian models for performance and dependability evaluation","author":"B.R. Haverkort","year":"2002","unstructured":"Haverkort B.R.: Markovian models for performance and dependability evaluation, pp. 38\u201383. Springer, New York (2002)"},{"key":"238_CR6","doi-asserted-by":"crossref","first-page":"1628","DOI":"10.1016\/j.ress.2008.01.007","volume":"93","author":"A.D. Dominguez-Garcia","year":"2008","unstructured":"Dominguez-Garcia A.D., Kassakianb J.G., Schindallb J.E., Zinchukc J.J.: An Integrated Methodology for the Dynamic Performance and Reliability Evaluation of Fault-tolerant Systems. Reliab. Eng. Syst. Saf. 93, 1628\u20131649 (2008)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"238_CR7","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M. Bozzano","year":"2007","unstructured":"Bozzano M., Villafiorita A.: The fsap\/nusmv-sa safety analysis platform. Int. J. Softw. Tools Technol. Transf. 9, 5\u201324 (2007). doi: 10.1007\/s10009-006-0001-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"238_CR8","first-page":"173","volume-title":"Computer Safety, Reliability, and Security, Lecture Notes in Computer Science, vol. 5775","author":"M. Bozzano","year":"2009","unstructured":"Bozzano M., Cimatti A., Katoen J.-P., Nguyen V., Noll T., Roveri M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds) Computer Safety, Reliability, and Security, Lecture Notes in Computer Science, vol. 5775, pp. 173\u2013186. Springer, Berlin (2009). doi: 10.1007\/978-3-642-04468-7_15"},{"key":"238_CR9","unstructured":"Gomes, A., Mota, A., Sampaio, A., Ferri, F., Buzzi, J.: Systematic model-based safety assessment via probabilistic model checking. In: Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation\u2014Part I, pp. 625\u2013639. ISoLA\u201910. Springer, Berlin (2010). http:\/\/dl.acm.org\/citation.cfm?id=1939281.1939338"},{"issue":"4","key":"238_CR10","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska M., Norman G., Parker D.: PRISM: probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Perform. Eval. Rev. 36(4), 40\u201345 (2009)","journal-title":"ACM SIGMETRICS Perform. Eval. Rev."},{"key":"238_CR11","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S., (eds.), 23rd International Conference on Computer Aided Verification (CAV\u201911), vol. 6806, pp. 585\u2013591. Springer, Snowbird, \u00c9tats-Unis (2011). http:\/\/hal.inria.fr\/hal-00648035"},{"key":"238_CR12","unstructured":"The MathWorks Inc.: Simulink Validation and Verification 2 User\u2019s Guide (2008)"},{"key":"238_CR13","doi-asserted-by":"crossref","unstructured":"Grunske, L., Colvin, R., Winter, K.: Probabilistic Model-Checking Support for FMEA. In: QEST \u201907: Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems, pp. 119\u2013128 (2007). doi: 10.1109\/QEST.2007.18","DOI":"10.1109\/QEST.2007.18"},{"key":"238_CR14","doi-asserted-by":"crossref","unstructured":"Joshi, A., Heimdahl, M.: Model-based safety analysis of Simulink models using SCADE design verifier. In: Winther, R., Gran, B., Dahll, G. (eds.) Computer Safety, Reliability, and Security. Lecture Notes in Computer Science. Springer, Berlin, vol. 3688, pp. 122\u2013135 (2005). doi: 10.1007\/11563228_10","DOI":"10.1007\/11563228_10"},{"key":"238_CR15","unstructured":"Akerlund, O., et\u00a0al.: ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proceedings of 3rd European Congress Embedded Real Time Software, ERTS 2006, Toulouse (France), 2006"},{"key":"238_CR16","volume-title":"Modeling Reactive Systems with Statecharts: The Statemate Approach","author":"D. Harel","year":"1998","unstructured":"Harel D., Politi M.: Modeling Reactive Systems with Statecharts: The Statemate Approach. McGraw-Hill, New York (1998)","edition":"1"},{"key":"238_CR17","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP\/NuSMV-SA safety analysis platform. In: Proceedings of SAFECOMP 2003. LNCS 2788, pp. 49\u201362. Springer, Edimburgh (2003)","DOI":"10.1007\/978-3-540-39878-3_5"},{"key":"238_CR18","unstructured":"DO-178B: Software Considerations in Airborne Systems and Equipment Certification (RTCA Inc.). Washington, DC, December 1996"},{"issue":"3","key":"238_CR19","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/S0951-8320(00)00076-4","volume":"71","author":"Y. Papadopoulos","year":"2001","unstructured":"Papadopoulos Y., McDermid J., Sasse R., Heiner G.: Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Reliab. Eng. Syst. Saf. 71(3), 229\u2013247 (2001)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"238_CR20","unstructured":"Lisagor, O., McDermid, J., Pumfrey, D.J.: Towards a practicable process for automated safety analysis. In: 24th International System Safety Conference, pp. 596\u2013607 (2006)"},{"key":"238_CR21","unstructured":"Papadopoulos, Y., Parker, D., Grante, C.: A method and tool support for model-based semi-automated failure modes and effects analysis of engineering designs. In: Proceedings of the 9th Australian workshop on Safety Critical Systems and Software. SCS \u201904, vol. 47, pp. 89\u201395. Australian Computer Society, Inc., Darlinghurst, Australia, 2004. http:\/\/dl.acm.org\/citation.cfm?id=1082338.1082348"},{"key":"238_CR22","doi-asserted-by":"crossref","unstructured":"Papadopoulos, Y., Maruhn, M.: Model-based synthesis of fault trees from matlab-simulink models, Dependable Systems and Networks, International Conference on (2001). doi: 10.1109\/DSN.2001.941393","DOI":"10.1109\/DSN.2001.941393"},{"key":"238_CR23","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Performance Evaluation of Complex Systems: Techniques and Tools, Performance 2002. Tutorial Lectures, pp. 261\u2013289. Springer, London (2002). http:\/\/dl.acm.org\/citation.cfm?id=647414.725162","DOI":"10.1007\/3-540-45798-4_12"},{"key":"238_CR24","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A markov reward model checker. In: Proceedings of the Second International Conference on the Quantitative Evaluation of Systems. IEEE Computer Society, Washington, DC, USA, pp. 243\u2013244 (2005). doi: 10.1109\/QEST.2005.2","DOI":"10.1109\/QEST.2005.2"},{"key":"238_CR25","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, E.V., Nordahl, J., Hansen, N.H.: From csp models to markov models. IEEE Trans. Softw. Eng. 19(6), 554\u2013570 (1993). doi: 10.1109\/32.232021","DOI":"10.1109\/32.232021"},{"key":"238_CR26","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Fabre, E., Haar, S.: Markov nets: probabilistic models for distributed and concurrent systems. In: IEEE Transactions on Automatic Control, IEEE Computer Society, pp. 1936\u20131950 (2003)","DOI":"10.1109\/TAC.2003.819076"},{"key":"238_CR27","doi-asserted-by":"crossref","unstructured":"Baier, C., Ciesinski, F., Marcus, G.: Probmela and verification of markov decision processes. SIGMETRICS Perform. Eval. Rev. 32(4), 22\u201327 (2005). doi: 10.1145\/1059816.1059821","DOI":"10.1145\/1059816.1059821"},{"key":"238_CR28","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7\u201348 (1999). doi: 10.1023\/A:1008739929481","DOI":"10.1023\/A:1008739929481"},{"key":"238_CR29","first-page":"269","volume-title":"Verifying Continuous Time Markov Chains","author":"A. Aziz","year":"1996","unstructured":"Aziz A., Sanwal K., Singhal V., Brayton R.: Verifying Continuous Time Markov Chains, pp. 269\u2013276. Springer, Berlin (1996)"},{"issue":"2","key":"238_CR30","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2005.10.030","volume":"153","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska M., Norman G., Parker D.: Quantitative analysis with the Probabilistic Model Checker PRISM. Electron. Notes Theor. Comput. Sci. 153(2), 5\u201331 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"238_CR31","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transf. 6(2), 128\u2013142 (2004). doi: 10.1007\/s10009-004-0140-2","DOI":"10.1007\/s10009-004-0140-2"},{"key":"238_CR32","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). doi: 10.1145\/359576.359585","DOI":"10.1145\/359576.359585"},{"key":"238_CR33","unstructured":"Oxford University Computing Laboratory: The PRISM Language-Semantics (2004). http:\/\/www.prismmodelchecker.org\/doc\/semantics.pdf"},{"key":"238_CR34","unstructured":"Damm, W., Franzle, M., Olderog, E.R., Podelski, A., Wilhelm, R., Herbstritt, M., Herbstritt, M., Wimmer, R., Peikenkamp, T., Bode, E., Adelaide, M., Johr, S., Hermanns, H., Becker, B.: Analysis of large safety-critical systems: A quantitative approach. In: Reports of SFB\/TR 14 AVACS 8 (2006)"},{"key":"238_CR35","unstructured":"Oxford University Computing Laboratory: Prism Model Checker (PRISM) (2004). http:\/\/www.prismmodelchecker.org\/"},{"key":"238_CR36","unstructured":"Jesus, J.B.J.: Designing and formal verification of fly-by-wire flight control systems. Master\u2019s thesis, Federal University of Pernambuco (2009)"},{"key":"238_CR37","doi-asserted-by":"crossref","unstructured":"Gomes, A.J.O.: Model based Safety Analysis using Probabilistic Model Checking. Master\u2019s thesis, Federal University of Pernambuco (2010)","DOI":"10.1007\/978-3-642-16558-0_50"},{"key":"238_CR38","doi-asserted-by":"crossref","DOI":"10.1201\/9781439863961","volume-title":"Reliable Computer System: Design and Evaluation","author":"D. Siewiorek","year":"1998","unstructured":"Siewiorek D., Swarz R.: Reliable Computer System: Design and Evaluation, 3rd edn. A K Peters\/CRC Press, Boca Raton (1998)","edition":"3"},{"key":"238_CR39","doi-asserted-by":"crossref","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M. Bozzano","year":"2011","unstructured":"Bozzano M., Cimatti A., Katoen J.-P., Nguyen V.Y., Noll T., Roveri M.: Safety, dependability and performance analysis of extended aadl models. Comput. J. 54, 754\u2013775 (2011). doi: 10.1093\/comjnl\/bxq024","journal-title":"Comput. J."},{"key":"238_CR40","doi-asserted-by":"crossref","unstructured":"Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Towards probabilistic modelling in event-b. In: Integrated Formal Methods\u2014IFM 2010. Lecture Notes in Computer Science, vol. 6396. Springer, Berlin, pp. 275\u2013289 (2010). http:\/\/hal.inria.fr\/inria-00524594\/en\/","DOI":"10.1007\/978-3-642-16265-7_20"},{"key":"238_CR41","unstructured":"The European Union ICT Project: Rigorous Open Development Environment for Complex Systems (RODIN) (2008). http:\/\/www.event-b.org\/"},{"key":"238_CR42","doi-asserted-by":"crossref","unstructured":"Bode, E., Peikenkamp, T., Rakow, J., Wischmeyer, S.: Model based importance analysis for minimal cut sets. In: Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, pp. 303\u2013317. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88387-6_27"},{"key":"238_CR43","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref\u2014a symbolic bisimulation tool box. In: ATVA 06, pp. 477\u2013492 (2006)","DOI":"10.1007\/11901914_35"},{"key":"238_CR44","doi-asserted-by":"crossref","unstructured":"Mota, A., Jesus, J., Gomes, A., Ferri, F., Watanabe, E.: Evolving a safe system design iteratively. In: Proceedings of the 29th International Conference on Computer Safety, Reliability, and Security. SAFECOMP\u201910, vol. 6351, pp. 361\u2013374. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15651-9_27"},{"key":"238_CR45","doi-asserted-by":"crossref","unstructured":"Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner-Fischer, F., Leue, S.: Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples. In: International Conference on Quantitative Evaluation of Systems, pp. 299\u2013308 (2009). doi: 10.1109\/QEST.2009.8","DOI":"10.1109\/QEST.2009.8"},{"key":"238_CR46","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/TNET.2008.923716","volume":"17","author":"Y. Xie","year":"2009","unstructured":"Xie Y., Yu S.-Z.: A large-scale hidden semi-Markov model for anomaly detection on user browsing behaviors. IEEE\/ACM Trans. Netw. 17, 54\u201365 (2009)","journal-title":"IEEE\/ACM Trans. Netw."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0238-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0238-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0238-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T08:58:56Z","timestamp":1642669136000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0238-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,6]]},"references-count":46,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11]]}},"alternative-id":["238"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0238-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,6]]}}}