001480961 000__ 05980cam\\22006017i\4500
001480961 001__ 1480961
001480961 003__ OCoLC
001480961 005__ 20231031003316.0
001480961 006__ m\\\\\o\\d\\\\\\\\
001480961 007__ cr\un\nnnunnun
001480961 008__ 230920s2023\\\\sz\a\\\\o\\\\\101\0\eng\d
001480961 020__ $$a9783031436819$$q(electronic bk.)
001480961 020__ $$a3031436814$$q(electronic bk.)
001480961 020__ $$z9783031436802
001480961 0247_ $$a10.1007/978-3-031-43681-9$$2doi
001480961 035__ $$aSP(OCoLC)1398310626
001480961 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dEBLCP$$dWSU
001480961 049__ $$aISEA
001480961 050_4 $$aQA76.9.F67
001480961 08204 $$a004.01/51$$223/eng/20230920
001480961 1112_ $$aInternational Workshop on Formal Methods for Industrial Critical Systems$$n(28th :$$d2023 :$$cAntwerp, Belgium)
001480961 24510 $$aFormal methods for industrial critical systems :$$b28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023, Proceedings /$$cAlessandro Cimatti, Laura Titolo, editors.
001480961 2463_ $$aFMICS 2023
001480961 264_1 $$aCham :$$bSpringer,$$c2023.
001480961 300__ $$a1 online resource (x, 260 pages) :$$billustrations (some color).
001480961 336__ $$atext$$btxt$$2rdacontent
001480961 337__ $$acomputer$$bc$$2rdamedia
001480961 338__ $$aonline resource$$bcr$$2rdacarrier
001480961 4901_ $$aLecture notes in computer science,$$x1611-3349 ;$$v14290
001480961 500__ $$aIncludes author index.
001480961 5050_ $$aIntro -- Preface -- Organization -- Contents -- Experimenting with Formal Verification and Model-Based Development in Railways: The Case of UMC and Sparx Enterprise Architect -- 1 Introduction -- 2 Related Work -- 3 MBSD, Sparx Enterprise Architect and UMC -- 3.1 Sparx Enterprise Architect -- 3.2 UML Model Checker -- 4 Methodology -- 5 Case Study -- 5.1 Model Checking Sparx EA Models -- 6 Lessons Learned and Limitations -- 7 Conclusion -- References -- The 4SECURail Case Study on Rigorous Standard Interface Specifications -- 1 Introduction -- 2 The Demonstrator Case Study
001480961 5058_ $$a2.1 The 4SECURail Case Study -- 2.2 The Formalization of the Case Study -- 3 Cost-Benefit Analysis -- 4 Discussion and Conclusions -- References -- Statistical Model Checking for P -- 1 Introduction -- 2 An Overview of P -- 2.1 An Overview of P and its Semantics -- 2.2 A Case Study: A Bike Sharing System -- 3 Statistical Model Checking with MultiVeStA -- 4 Integration of P and MultiVeStA -- 5 A Case Study -- 5.1 Verifying Quantitative Properties of the Bikes Example -- 5.2 On the Scalability of Statistical Model Checking -- 6 Concluding Remarks -- References
001480961 5058_ $$aPattern-Based Verification of ROS 2 Nodes Using UPPAAL -- 1 Introduction -- 2 Background -- 2.1 ROS 2 -- 2.2 Timed Automata and UPPAAL -- 3 Modeling and Verification of ROS 2 Nodes in UPPAAL -- 4 Evaluation of Pattern-Based Verification -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers -- 1 Introduction -- 2 Preliminaries -- 2.1 Railway Interlocking System and its Object Manager Subsystem -- 2.2 Component Integration and Test Generation Approach
001480961 5058_ $$a2.3 VIATRA Query Language -- 3 Configuring Message Queues for Component Interactions -- 4 Property Specification Using Model Queries -- 5 Practical Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Refinement of Systems with an Attacker Focus -- 1 Introduction -- 2 Modelling Systems and Attacks -- 3 Attacker Objectives -- 4 Refinement Checking -- 5 Implementation -- 6 Case Study -- 6.1 Amazon Delivery -- 6.2 Duqu Malware -- 7 Conclusion -- References -- Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control -- 1 Introduction
001480961 5058_ $$a2 Case House and Problem Statement -- 3 Buffer Tank and Mixing Loop Thermodynamics -- 4 System Modelling in Uppaal Stratego -- 4.1 Buffer Tank Modelling in Uppaal Stratego -- 4.2 Online Synthesis -- 5 Experimental Evaluation -- 5.1 Evaluation Setup -- 5.2 Buffer Tank Quality Assessment -- 5.3 Buffer Tank Evaluations with Intelligent Stratego Controller -- 5.4 Mixing Loop Evaluations with Intelligent Stratego Controller -- 6 Conclusion -- References -- Automated Property-Based Testing from AADL Component Contracts -- 1 Introduction -- 2 Background -- 3 Example
001480961 506__ $$aAccess limited to authorized users.
001480961 520__ $$aThis book constitutes the proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, held in Antwerp, Belgium, during September 20-22, 2023. The 14 full papers included in this book were carefully reviewed and selected from 24 submissions. The papers focus on development and application of formal methods in industry. FMICS is a platform for scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. FMICS also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
001480961 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed September 20, 2023).
001480961 650_0 $$aFormal methods (Computer science)$$vCongresses.$$vCongresses$$0(DLC)sh2008104061
001480961 650_0 $$aSoftware engineering$$vCongresses.$$vCongresses$$0(DLC)sh2008111658
001480961 655_0 $$aElectronic books.
001480961 655_7 $$aConference papers and proceedings.$$2lcgft
001480961 7001_ $$aCimatti, Alessandro,$$eeditor.$$1https://orcid.org/0000-0002-1315-6990
001480961 7001_ $$aTitolo, Laura,$$eeditor.$$1https://orcid.org/0000-0001-7820-7640
001480961 830_0 $$aLecture notes in computer science ;$$v14290.$$x1611-3349
001480961 852__ $$bebk
001480961 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-031-43681-9$$zOnline Access$$91397441.1
001480961 909CO $$ooai:library.usi.edu:1480961$$pGLOBAL_SET
001480961 980__ $$aBIB
001480961 980__ $$aEBOOK
001480961 982__ $$aEbook
001480961 983__ $$aOnline
001480961 994__ $$a92$$bISE