000 04230nam a22005295i 4500
001 978-3-031-33163-3
003 DE-He213
005 20240730203551.0
007 cr nn 008mamaa
008 230514s2023 sz | s |||| 0|eng d
020 _a9783031331633
_9978-3-031-33163-3
024 7 _a10.1007/978-3-031-33163-3
_2doi
050 4 _aQA267-268.5
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a005.131
_223
245 1 0 _aRigorous State-Based Methods
_h[electronic resource] :
_b9th International Conference, ABZ 2023, Nancy, France, May 30-June 2, 2023, Proceedings /
_cedited by Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque.
250 _a1st ed. 2023.
264 1 _aCham :
_bSpringer Nature Switzerland :
_bImprint: Springer,
_c2023.
300 _aXIII, 380 p. 131 illus., 107 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v14010
505 0 _aPattern-based Refinemnt Generation Through Domain Specifi Languages -- Inductive Construction in B with the Theory Plugin -- Validation of Formal Models by Interactive Simulation -- Thread-Local, Step-Local Proof Obligations for Refnement of State-Based Concurrent Systems -- Encoding TLA+ Proof Obligations Safely for SMT -- Compositional I/O Abstract State Machines -- Crucible Tools for Test Generation and Animation of Alloy Models -- Modelling an Automotive Software System with TASTD -- TASTD a real-time extension for ASTD -- Validation by Abstraction and Refiement -- Verifying Event-B Hybrid Models using Cyclone -- Exploration of Reflectie ASMs for Security -- Standalone Event-B models analysis relying on the EB4EB meta-theory -- Adding records to Alloy -- Designing Secure Systems using Hierarchical STPA and Event-B -- Behavioural Theory of Reflectie Algorithms -- Specification in the Event-B Institution -- Verifying temporal relational models with Pardinus -- AMAN Case Study -- Analysis of a Safety-critical Interactive System through VOs -- Task Model Design and Analysis with Alloy -- Modeling and Verifying an Arrival Manager using Event-B -- Formal MVC: a Pattern for the Integration of ASM Specification in UI Development -- Exploring a methodology for formal verificatio of safety-critical systems -- Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems -- A framework for formal verificatio and validation of railway systems -- Reconstruction of TLAPS proofs solved by veriT in Lambdapi.
520 _aThis book constitutes the refereed proceedings of the 9th International Conference on Rigorous State-Based Methods, ABZ 2023, held in Nancy, France, in May 2023. The 12 full and 7 short papers included in this volume were carefully reviewed and selected from 47 submissions. The proceedings also include 4 PhD symposium contributions. They deal with state-based and machine-based formal methods, mainly Abstract State Machines (ASM), Alloy, B, TLA+, VDM, and Z. .
650 0 _aMachine theory.
_9176627
650 1 4 _aFormal Languages and Automata Theory.
_9176628
700 1 _aGlässer, Uwe.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9176629
700 1 _aCreissac Campos, Jose.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9176630
700 1 _aMéry, Dominique.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9176631
700 1 _aPalanque, Philippe.
_eeditor.
_0(orcid)
_10000-0002-5381-971X
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9176632
710 2 _aSpringerLink (Online service)
_9176633
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031331626
776 0 8 _iPrinted edition:
_z9783031331640
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v14010
_923263
856 4 0 _uhttps://doi.org/10.1007/978-3-031-33163-3
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c97562
_d97562