Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola: 12th International Symposium, ISoLA 2024, Proceedings, Part I 1

The ISoLA 2024 proceedings constitutes contributions of the associated events held at the 12th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2024, which took place in Crete, Greece, in October 2024. ISoLA 2024 provides a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools and methods for the specification, analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their different application domains. This volume, Part I, contains the proceedings of the Colloquium in honor of Rocco De Nicola’s 70th birthday, held jointly with the ISOLA 2024’s track on REoCAS (Rigorous Engineering of Collective Adaptive Systems). Rocco De Nicola has significantly contributed to collective adaptive systems through novel approaches for their formal specification, analysis, and verification. The Colloquium features one homage paper and 23 contributions from invited authors who reflected upon these developments within the context of Rocco’s much broader legacy in concurrency theory, distributed systems, domain-specific languages, service-oriented computing, and formal methods, exploring his recent contributions to cybersecurity. Preface Organization Contents – Part I Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola's 70th Birthday 1 Introduction 2 Overview of Contributions 3 Concluding Remarks References Systems Security Modeling and Analysis at IMT Lucca 1 Introduction 2 Cybersecurity 3 Teaching 4 Some Personal Reflections 5 Conclusion References Klaim in the Making 1 Introduction 2 Klaim: The First Steps 3 The Implementations 3.1 Implementation in Ada 3.2 Implementation in Java 4 The Impact of Klaim 4.1 AGILE and MIKADO 4.2 SENSORIA 4.3 ASCENS 5 Laudatio References Formal Approaches for Modeling and Analysis of Business Process Collaborations 1 Introduction 2 Background Notions 3 BPMN Collaboration Diagrams: Formalisation and Verification 4 BPMN Collaboration Diagrams: Extended Framework 5 Concluding Remarks References An Abstract Account of Up-to Techniques for Inductive Behavioural Relations 1 Introduction 2 Inductive Observables and Weights 2.1 Inductive Observables 2.2 Weights 3 Functions for Inductive Enhancements 4 Complete Lattices and Chains of Approximants 4.1 Post-Fixed Points and Chains 4.2 Monotone Functions 4.3 From Complete Lattices to Behavioural Relations 5 Concluding Remarks 5.1 Related Work 5.2 Further Developments References Language Equivalence from Nondeterministic to Weighted Automata—and Back 1 Introduction 2 Preliminaries: NFAs and Language Equivalence 3 Weighted Automata Over a Field 4 Back to NFA: Quotients and State Reduction 5 Complexity and Implementation 5.1 Complexity 5.2 Vectorized Implementation 6 Evaluation 7 Conclusion References A Process Algebraic View of In/Out Prisoners 1 Introduction 2 Background 3 The Puzzle 3.1 The Solution to the Puzzle 4 Modelling the Puzzle in CCS 4.1 Modularity 4.2 Process Equivalences 4.3 Model Checking 5 Playing with CAAL 5.1 Edit Panel 5.2 Explore Panel 5.3 Verify Panel 5.4 Further Experimentation 6 Concluding Remarks References Towards a Formal Testing Theory for Quantum Processes 1 Introduction 2 Formal Testing Theory: Available Results 2.1 Testing Theories for Discrete Systems 2.2 Testing Theories for Probabilistic Systems 3 Quantum Systems and Process Theories 3.1 Quantum Systems: Brief Introduction 3.2 Quantum Process Theories 4 Quantum Testing Pre-orders: Requirements and Challenges 4.1 Requirements 4.2 Challenges 5 Quantum Testing Pre-orders: Future Roadmap 6 Conclusions References Testing Quantum Processes 1 Introduction 2 Background 2.1 Probability Distributions 2.2 Quantum Computing 2.3 Density Operator Formalism 3 A Quantum Process Algebra 3.1 Syntax and Type System 3.2 Operational Semantics 4 Testing Equivalences 4.1 Testing Semantics 4.2 Testing Equivalence 4.3 The Problem of Non-deterministic Testing 5 Conclusions and Future Work A Full Type System B Proofs References The ProbInG Project: Advancing Automatic Analysis of Probabilistic Loops 1 Introduction 2 Prob-Solvable Loops 3 Bayesian Networks as Prob-Solvable Loops 4 Probabilistic Loops with Non-polynomial Updates 5 Automated Termination Analysis 6 (Un)Solvable Loops 7 Conclusion and Future Work References Towards a Probabilistic Programming Approach to Analyse Collective Adaptive Systems 1 Introduction 2 Markov Population Process 2.1 Expansion of the CME 2.2 Sampling Methods 3 MPPs as Probabilistic Programs 3.1 SOGA in a Nutshell 3.2 SOGA-MPP: SOGA Analysis for MPPs 4 Experiments 5 Conclusion References Can AI Help with the Formalization of Railway Cybersecurity Requirements? 1 Introduction 2 Translating Railway Requirements Into CNL4DSA 2.1 ERTMS L3 Signalling System Security Requirements 3 Prompting Methodology 4 Ask ChatGPT! 5 Ask Copilot! 6 Related Work 7 Conclusion References White-Box Validation of Collective Adaptive Systems by Statistical Model Checking and Process Mining 1 Introduction 2 A Collision Avoidance Robotics Scenario 3 Background 3.1 SCEL 3.2 Process Mining 4 Recent Developments on Integrating Statistical Model Checking and Process Mining 5 Methodology Applied on the Scenario 5.1 SMC Analysis Results 5.2 Identifying and Solving Issues in the Model with PM 5.3 Diff Model 6 Conclusions References Analysing Collective Adaptive Systems by Proving Theorems 1 Introduction 2 Brief Overview of Frameworks for Ensembles 2.1 A Different Approach 3 Formalisation 4 Simulation 5 Verification 6 Make it Concrete 6.1 Ants in an SMT-Solver 6.2 Ants in Higher-Order Logic 6.3 Finding the Right Path 7 Conclusions References Engineering Ethical-Aware Collective Adaptive Systems 1 Introduction 2 Background and Motivating Scenario 2.1 A Motivating Scenario 3 CASs: Where We Are 4 Challenges for Engineering Ethical-Aware Collective Adaptive Systems 5 Conclusion References Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification 1 Introduction 2 Modelling the Audience 3 Analysis 4 Conclusion and Related Work References Flocks of Birds: A Quantitative Evaluation 1 Introduction 2 Related Work 3 Flocks of Birds: A Stochastic Model 3.1 Scenarios Under Analysis 3.2 An MPP Semantics for Flocks of Birds 3.3 Fluid Approximation 4 Flocks of Birds: Quantitative Analysis 4.1 Evaluation Without Cohesion 4.2 Evaluation with Cohesion 4.3 Evaluation of a Prey Before Cohesion 4.4 Evaluation of a Prey After Cohesion 5 Discussion 6 Conclusion and Future Work References Strategies in Spatio-Temporal Logics for Multi-agent Systems 1 Introduction 2 Related Work 3 Situated Behaviours: Some Motivating Examples 3.1 Mobile ad Hoc networks 3.2 Transportation Networks 3.3 The Use of Strategies 4 Background 4.1 Meet-Semilattices and Trees 4.2 Meet-Semilattices in Temporal Observation 4.3 Meet-Semilattices in Spatial Observation 4.4 Meet-Semilattices and Kripke Structures 4.5 Concurrent Game Structures 5 A Categorical Semantics for a Spatial and Temporal Logic 5.1 Logics for Subobjects 5.2 Modal Logic 6 Extending Logics to Strategies 7 Combining Space and Time 8 Conclusions References Function-as-a-Service Allocation Policies Made Formal 1 Introduction 2 An Informal Introduction to APP 3 Operational Semantics of APP 4 Related Work 5 Conclusion and Future Work References Asynchronous Multiparty Sessions with Internal Delegation 1 Introduction 2 Multiparty Sessions 3 Type System 4 Properties of Typable Sessions 5 Related Work and Conclusion References Code-Centric Code Generation 1 Introduction 2 Related Work 3 CCG Approach 3.1 Prototyping 3.2 Building the CCG Tree 3.3 Operation Annotation 3.4 Template Generation 3.5 Target Generation 3.6 Evolution 4 Evaluation 5 Conclusion and Future Work References Attack Tree Generation via Process Mining 1 Introduction 2 Background 2.1 Attack Trees 2.2 Process Trees 2.3 Process Mining 3 From Process Trees to Attack Trees 3.1 Attack Tree Semantics 3.2 Process Tree Semantics 3.3 Basics of the Transformations 3.4 Transformation Rules 4 Reconstructing Attack Trees Generated by RisQFlan 5 Related Work 6 Conclusion and Future Work References Local Spaces in Soft Concurrent Constraint Programming Oriented to Security 1 Introduction 2 Semiring-Based Soft Constraints 2.1 Soft Constraint Systems 3 Space Functions in a Soft World 4 An Application to a Security-Oriented SCCP Language 4.1 An Operational Semantics 5 Related Work 5.1 Shared Spaces in Concurrent Languages 5.2 Shared Spaces in Constraint Languages 6 Conclusion References Riding the Data Storms: Specifying and Analysing IoT Security Requirements with SURFING 1 Introduction 2 Smart Street Light Control System 3 Surfing Executor 4 Symbolic Surfing 5 Concluding Remarks References Preventing Out-of-Gas Exceptions by Typing 1 Introduction 2 TinySol with Gas and Exceptions 3 A Small-Step Semantics with Exceptions and Gas 4 A Type System for Termination 4.1 The Type System 4.2 Properties of the Type System 4.3 Limitations of the Type System 5 Conclusion and Future Work References Author Index