LEADER 05827nam 2200529 450 001 996464409603316 005 20231110225034.0 010 $a3-030-90636-1 035 $a(CKB)4940000000615734 035 $a(MiAaPQ)EBC6799127 035 $a(Au-PeEL)EBL6799127 035 $a(OCoLC)1284917771 035 $a(PPN)258838639 035 $a(EXLCZ)994940000000615734 100 $a20220729d2021 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aFormal aspects of component software $e17th international conference, FACS 2021, virtual event, October 28-29, 2021 : proceedings /$fedited by Gwen Salau?n and Anton Wijs 210 1$aCham, Switzerland :$cSpringer,$d[2021] 210 4$d©2021 215 $a1 online resource (182 pages) 225 1 $aLecture Notes in Computer Science ;$vv.13077 311 $a3-030-90635-3 320 $aIncludes bibliographical references and index. 327 $aIntro -- Preface -- Organization -- Parametric and Interval Model Checking: Recent Advances and Applications (Abstract of Invited Paper) -- Contents -- Invited Paper -- Learning Assumptions for Verifying Cryptographic Protocols Compositionally -- 1 Introduction -- 2 Background -- 2.1 Labeled Transition Systems -- 2.2 Assumption Learning and Alphabet Refinement -- 3 An Overview of Taglierino -- 4 The Attacker Model and Its Correctness -- 5 Protocol Analysis -- 5.1 Evaluation Setup -- 5.2 Needham-Schroeder-Lowe -- 5.3 Denning-Sacco -- 5.4 Woo-Lam -- 5.5 Kerberos -- 5.6 Performance Evaluation Results -- 6 Related Work -- 7 Conclusion -- References -- Modelling and Composition -- Component-Based Approach Combining UML and BIP for Rigorous System Design -- 1 Introduction -- 2 System Modeling with UML -- 2.1 Case Study -- 2.2 Architecture Model -- 2.3 Behavior Models -- 3 From UML to BIP -- 4 System Simulation and Verification -- 5 Related Work -- 6 Conclusion -- References -- Composable Partial Multiparty Session Types -- 1 Introduction -- 2 A Calculus for Processes over Multiparty Sessions -- 3 Partial Multiparty Session Types -- 4 Type System -- 5 Merging Partial Session Types -- 5.1 Mapping Merging Functions over Session Types -- 5.2 Merging Communications and Session Types -- 6 Subject Reduction and Progress -- 7 Related Work -- 8 Conclusions -- References -- A Canonical Algebra of Open Transition Systems -- 1 Introduction -- 1.1 State from Feedback -- 1.2 The Algebra of Transition Systems -- 1.3 Stateful and Stateless Components -- 1.4 Canonicity and Our Original Contribution -- 1.5 Related Work -- 1.6 Synopsis -- 1.7 Conventions -- 2 Preliminaries: Categories with Feedback -- 2.1 Categories with Feedback -- 2.2 Traced Monoidal Categories -- 2.3 Delay and Feedback -- 2.4 St(), the Free Category with Feedback -- 2.5 Examples. 327 $a3 Span(Graph): An Algebra of Transition Systems -- 3.1 The Algebra of Span(Graph) -- 3.2 The Components of Span(Graph) -- 3.3 Span(Graph) as a Category with Feedback -- 3.4 Cospan(Graph) as a Category with Feedback -- 3.5 Syntactical Presentation of Cospan(FinGraph) -- 4 Conclusions and Further Work -- References -- Corinne, a Tool for Choreography Automata -- 1 Introduction -- 2 Choreography Automata -- 3 Corinne -- 4 Conclusion, Related Work, and Future Work -- References -- Verification -- Specification and Safety Verification of Parametric Hierarchical Distributed Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Term Algebra of Behaviors -- 4 The Parametric Safety Problem -- 4.1 Encoding Invariants and Error Configurations -- 4.2 The Flow of a Behavioral Term -- 5 Experimental Evaluation -- 6 Related Work -- 7 Conclusions and Future Work -- References -- A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions -- 1 Introduction -- 2 Preliminaries -- 2.1 The PRAM Model -- 2.2 Strong Bisimulation -- 3 Relational Coarsest Partition Problem -- 3.1 The Sequential Algorithm -- 3.2 The PRAM Algorithm -- 3.3 Correctness -- 3.4 Complexity Analysis -- 4 Bisimulation Coarsest Refinement Problem -- 4.1 The PRAM Algorithm -- 4.2 Complexity and Correctness -- 5 Experimental Results -- 5.1 Experimental Comparison -- 6 Conclusion -- References -- Automated Generation of Initial Configurations for Testing Component Systems -- 1 Introduction -- 2 Background -- 3 Component-Based Model -- 4 Generation of Initial Configurations -- 4.1 Combinatorial Algorithm -- 4.2 Initial Configuration Sampling -- 4.3 Integration into the Online Test Generation Process -- 5 Experimentation -- 6 Related Work -- 7 Conclusion and Future Works -- References -- Monitoring Distributed Component-Based Systems -- 1 Introduction. 327 $a2 Preliminaries and Notations -- 3 Distributed CBS -- 3.1 Semantics -- 3.2 Traces -- 4 Efficient Construction of the Computation Lattice -- 4.1 Computation Lattice -- 4.2 Intermediate Operations -- 4.3 Algorithms for Constructing the Computation Lattice -- 5 Properties of the Constructed Lattice -- 5.1 Insensitivity to Communication Delay -- 5.2 Correctness of Lattice Construction -- 6 Related Work -- 7 Conclusions -- References -- Author Index. 410 0$aLecture Notes in Computer Science 606 $aSoftware engineering$vCongresses 606 $aFormal methods (Computer science)$vCongresses 606 $aComponent software$vCongresses 615 0$aSoftware engineering 615 0$aFormal methods (Computer science) 615 0$aComponent software 676 $a004.0151 702 $aSalau?n$b G$g(Gwen), 702 $aWijs$b Anton 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996464409603316 996 $aFormal Aspects of Component Software$92968343 997 $aUNISA