{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,16]],"date-time":"2024-06-16T07:17:09Z","timestamp":1718522229096},"reference-count":20,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2017,1,3]],"date-time":"2017-01-03T00:00:00Z","timestamp":1483401600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"Verification of safety requirements is one important task during the development of safety critical systems. The increasing complexity of systems makes manual analysis almost impossible. This paper introduces a new methodology for formal verification of technical systems with smartIflow (State Machines for Automation of Reliability-related Tasks using Information FLOWs). smartIflow is a new modeling language that has been especially designed for the purpose of automating the safety analysis process in early product life cycle stages. It builds up on experience with existing approaches. As is common practice in current approaches, components are modeled as finite state machines. However, new concepts are introduced to describe component interactions. Events play a major role for internal interactions between components as well as for external (user) interactions. Our approach to the verification of formally specified safety requirements is a two-step method. First, an exhaustive simulation creates knowledge about a great variety of possible behaviors of the system, especially including reactions on suddenly occurring (possibly intermittent) faults. In the second step, safety requirements specified in CTL (Computation Tree Logic) are verified using model checking techniques, and counterexamples are generated if these are not satisfied. The practical applicability of this approach is demonstrated based on a Java implementation using a simple Two-Tank-Pump-Consumer system.<\/jats:p>","DOI":"10.3390\/info8010007","type":"journal-article","created":{"date-parts":[[2017,1,3]],"date-time":"2017-01-03T15:26:49Z","timestamp":1483457209000},"page":"7","source":"Crossref","is-referenced-by-count":12,"title":["Model Based Safety Analysis with smartIflow"],"prefix":"10.3390","volume":"8","author":[{"given":"Philipp","family":"H\u00f6nig","sequence":"first","affiliation":[{"name":"Ulm University of Applied Sciences, Department of Computer Science, 89075 Ulm, Germany"}]},{"given":"R\u00fcdiger","family":"Lunde","sequence":"additional","affiliation":[{"name":"Ulm University of Applied Sciences, Department of Computer Science, 89075 Ulm, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-4733-9186","authenticated-orcid":false,"given":"Florian","family":"Holzapfel","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Institute of Flight System Dynamics, 85748 Garching, Germany"}]}],"member":"1968","published-online":{"date-parts":[[2017,1,3]]},"reference":[{"key":"ref_1","unstructured":"Federal Aviation Administration (FAA) (2000). FAA System Safety Handbook, Federal Aviation Administration."},{"key":"ref_2","unstructured":"Lunde, K., Lunde, R., and M\u00fcnker, B. (29\u20131, January 29). Model-Based Failure Analysis with RODON. Proceedings of the 2006 Conference on ECAI 2006: 17th European Conference on Artificial Intelligence, Riva Del Garda, Italy."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Batteux, M., Prosvirnova, T., Rauzy, A., and Kloul, L. (2013, January 29\u201331). The AltaRica 3.0 project for model-based safety assessment. Proceedings of the 2013 11th IEEE International Conference on Industrial Informatics (INDIN), Bochum, Germany.","DOI":"10.1109\/INDIN.2013.6622976"},{"key":"ref_4","unstructured":"Papadopoulos, Y., and McDermid, J.A. (1999). Computer Safety, Reliability and Security, Springer."},{"key":"ref_5","unstructured":"H\u00f6nig, P., and Lunde, R. (2014, January 8\u201311). A New Modeling Approach for Automated Safety Analysis Based on Information Flows. Proceedings of the 25th International Workshop on Principles of Diagnosis (DX14), Graz, Austria."},{"key":"ref_6","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking (Representation and Mind Series), The MIT Press."},{"key":"ref_7","unstructured":"NuSMV 2.5 User Manual. Available online: http:\/\/nusmv.fbk.eu\/NuSMV\/userman\/v25\/nusmv.pdf."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Huth, M., and Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press.","DOI":"10.1017\/CBO9780511810275"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Lisagor, O., Kelly, T., and Niu, R. (2011, January 12\u201315). Model-based safety assessment: Review of the discipline and its challenges. Proceedings of the 2011 9th International Conference on Reliability, Maintainability and Safety (ICRMS), Guiyang, China.","DOI":"10.1109\/ICRMS.2011.5979344"},{"key":"ref_10","unstructured":"Simscape. Available online: https:\/\/www.mathworks.com\/products\/simscape.html."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/381766.381770","article-title":"Towards Integrated Integrated Safety Analysis and Design","volume":"2","author":"Fenelon","year":"1994","journal-title":"ACM Appl. Comput. Rev."},{"key":"ref_12","unstructured":"Struss, P., and Dobi, S. (2013, January 1\u20134). Automated Functional Safety Analysis of Vehicles Based on Qualitative Behavior Models and Spatial Representations. Proceedings of the 24th International Workshop on Principles of Diagnosis (DX-2013), Jerusalem, Israel."},{"key":"ref_13","unstructured":"Simulink. Available online: https:\/\/www.mathworks.com\/products\/simulink\/."},{"key":"ref_14","unstructured":"Joshi, A., Whalen, M., and Heimdahl, M.P. (2005). ModelBased Safety Analysis: Final Report, University of Minnesota. Technical Report."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., and Roveri, M. (2009, January 15\u201318). The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. Proceedings of the 28th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2009, Hamburg, Germany.","DOI":"10.1007\/978-3-642-04468-7_15"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Gudemann, M., and Ortmeier, F. (2010, January 3\u20134). A Framework for Qualitative and Quantitative Formal Model-Based Safety Analysis. Proceedings of the 2010 IEEE 12th International Symposium on High-Assurance Systems Engineering (HASE), San Jose, CA, USA.","DOI":"10.1109\/HASE.2010.24"},{"key":"ref_17","unstructured":"Lunde, R. (2006). Towards Model-Based Engineering: A Constraint-Based Approach, Shaker."},{"key":"ref_18","unstructured":"H\u00f6nig, P., Lunde, R., and Holzapfel, F. (2015, January 8\u201310). Modeling Technical Systems with smartIflow for Safety Related Tasks. Proceedings of the International Workshop on Applications in Information Technology (IWAIT-2015), Aizu-Wakamatsu, Japan."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Popeea, C., and Rybalchenko, A. (2016, January 3). Efficient CTL Verification via Horn Constraints Solving. Proceedings of the 3rd Workshop on Horn Clauses for Verification and Synthesis, San Francisco, CA, USA.","DOI":"10.4204\/EPTCS.219.1"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1613\/jair.3898","article-title":"Qualitative Order of Magnitude Energy-Flow-Based Failure Modes and Effects Analysis","volume":"46","author":"Snooke","year":"2013","journal-title":"J. Artif. Intell. Res."}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/8\/1\/7\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T19:17:31Z","timestamp":1717701451000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/8\/1\/7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,3]]},"references-count":20,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2017,3]]}},"alternative-id":["info8010007"],"URL":"https:\/\/doi.org\/10.3390\/info8010007","relation":{},"ISSN":["2078-2489"],"issn-type":[{"value":"2078-2489","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1,3]]}}}