Formal aspects of component software : 18th international conference, FACS 2022, virtual event, November 10-11, 2022, proceedings / / Silvia Lizeth Tapia Tarifa, José Proença (editors)

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (252 pages)
• Disciplina: 005.3
• Soggetto topico: Component software; Formal methods (Computer science); Software engineering
• Persona (resp. second.): ProençaJosé; Tapia TarifaSilvia Lizeth
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- Preface -- Organization -- Contents -- Modelling and Verification -- Compositional Simulation of Abstract State Machines for Safety Critical Systems -- 1 Introduction -- 2 The Mechanical Ventilator Milano (MVM) Case Study -- 2.1 Problem Context -- 2.2 System Behavioral Description -- 3 Preliminary Concepts on ASMs and ASMETA -- 3.1 Modeling Example -- 3.2 The ASMETA (ASM mETAmodeling) Toolset -- 4 Compositional Simulation of ASM Models -- 5 Compositional Modeling and Simulation at Work -- 6 Discussion and Lesson Learned -- 7 Related Work -- 8 Conclusion and Future Directions -- References -- Specifying Source Code and Signal-based Behaviour of Cyber-Physical System Components -- 1 Introduction -- 2 Motivation and Language Design Goals -- 3 Background -- 3.1 Traces for Signals Used by HLS ch2Menghi2020 -- 3.2 Traces for Source Code Used by iCFTL ch2DawesRV2021 -- 4 Hybrid Traces -- 5 SCSLSyntax -- 5.1 Examples -- 6 Semantics -- 6.1 Determining Values of Terms -- 6.2 A Semantics Function -- 7 Language Comparison -- 7.1 Implications for Software Verification and Validation Processes -- 8 Ongoing Work -- 9 Conclusion -- References -- Formally Characterizing the Effect of Model Transformations on System Properties -- 1 Introduction -- 2 Related Work -- 3 Background -- 4 Formalized Model Transformations -- 5 Transformation Characterization -- 5.1 Merging the ALTL Formula and the -extended LTS L -- 5.2 Transforming L_ -- 5.3 Detecting and Removing Non-Accepting Cycles in T(L_) -- 5.4 Constructing a Characteristic Formula for T(L_)_ -- 6 A Progress Example -- 7 Conclusions -- References -- Interpretation and Formalization of the Right-of-Way Rules -- 1 Introduction -- 2 Formalization of Right-of-Way Rules -- 2.1 Basic Definitions -- 2.2 Convergence, Divergence, and Overtake -- 3 Properties of the Right-of-Way Rules. ; 4 Comparison with Previous Formalization -- 4.1 Converging -- 4.2 Head-On or Nearly So -- 4.3 Overtaking -- 4.4 Right-of-Way -- 5 Aspects of the Right-of-Way Rules Formalization -- 6 Summary and Conclusion -- References -- Formal Model In-The-Loop for Secure Industrial Control Networks -- 1 Introduction -- 2 Background -- 3 System Architecture -- 4 Black Box Model -- 5 White Box Model -- 6 Results and Comparisons -- 7 Related Work -- 8 Conclusion -- References -- Debugging of BPMN Processes Using Coloring Techniques -- 1 Introduction -- 2 Background -- 3 BPMN Coloration -- 3.1 Overview -- 3.2 Folding -- 4 Tool and Experiments -- 4.1 Tool -- 4.2 Empirical Study -- 4.3 Performance Study -- 5 Related Work -- 6 Concluding Remarks -- References -- WEASY: A Tool for Modelling Optimised BPMN Processes -- 1 Introduction -- 2 Models -- 3 Tool -- 4 Experiments -- 5 Case Study -- 6 Concluding Remarks -- References -- Logics and Semantics -- Embeddings Between State and Action Based Probabilistic Logics -- 1 Introduction -- 2 Discrete-Time Markov Chains -- 3 Modified Embeddings sld and ald -- 4 State Based Logics -- 4.1 PCTL -- 4.2 PCTL* -- 5 Action Based Logics -- 5.1 prHML -- 5.2 APCTL* -- 5.3 APCTL -- 6 Embeddings for Probabilistic Logics -- 6.1 PCTL*APCTL* -- 6.2 APCTL*PCTL* -- 6.3 PCTLAPCTL -- 6.4 APCTLPCTL -- 7 Related Work -- 8 Conclusion -- References -- Footprint Logic for Object-Oriented Components -- 1 Introduction -- 2 The Programming Language -- 3 The Specification Language -- 4 The Hoare Logic of Footprints -- 5 A Comparison Between Related Approaches -- 5.1 Footprints -- 5.2 Dynamic Frames -- 5.3 Separation Logic -- 6 Discussion -- 7 Conclusion -- References -- Decompositional Branching Bisimulation Minimisation of Monolithic Processes -- 1 Introduction -- 2 mCRL2 -- 3 Cleave and Combine -- 4 Extension to Branching Bisimilarity -- 5 Minimisation. ; 6 Experimental Results -- 7 Conclusion -- References -- Types and Choreographies -- Realisability of Branching Pomsets -- 1 Introduction -- 2 Preliminaries on Branching Pomsets -- 3 Realisability -- 4 Well-formedness -- 5 Bisimulation Proof -- 6 Examples -- 7 Related Work -- 8 Conclusion -- References -- Liquidity Analysis in Resource-Aware Programming -- 1 Introduction -- 2 The Stipula Language -- 3 Semantics -- 4 The Theory of Liquidity -- 5 The Algorithm for Liquidity -- 6 Related Works -- 7 Conclusions -- References -- Open Compliance in Multiparty Sessions -- 1 Introduction -- 2 Calculus -- 3 Type System -- 4 Open Compliance -- 5 Concluding Remarks, Related and Future Works -- References -- Author Index.
• Titolo autorizzato: Formal Aspects of Component Software
• ISBN: 3-031-20872-2
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996500066603316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture notes in computer science ; ; Volume 13712.