LEADER 04196nam 2200577 a 450 001 9910483536203321 005 20200520144314.0 024 7 $a10.1007/11576280 035 $a(CKB)1000000000213336 035 $a(SSID)ssj0000317704 035 $a(PQKBManifestationID)11258695 035 $a(PQKBTitleCode)TC0000317704 035 $a(PQKBWorkID)10294160 035 $a(PQKB)11401971 035 $a(DE-He213)978-3-540-32250-4 035 $a(MiAaPQ)EBC3067537 035 $a(PPN)123098424 035 $a(EXLCZ)991000000000213336 100 $a20050926d2005 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFormal methods and software engineering $e7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005 : proceedings /$fKung-Kiu Lau, Richard Banach (eds.) 205 $a1st ed. 2005. 210 $aBerlin ;$aNew York $cSpringer$d2005 215 $a1 online resource (XIV, 502 p.) 225 1 $aLecture notes in computer science,$x0302-9743 ;$v3785 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$aPrinted edition: 9783540297970 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Realising the Benefits of Formal Methods -- A Compositional Framework for Service Interaction Patterns and Interaction Flows -- An Evidential Tool Bus -- Specification -- Derivation of UML Class Diagrams as Static Views of Formal B Developments -- 29 New Unclarities in the Semantics of UML 2.0 State Machines -- The Semantics and Tool Support of OZTA -- Modelling -- An Abstract Model for Process Mediation -- How Symbolic Animation Can Help Designing an Efficient Formal Model -- Security -- A Theory of Secure Control Flow -- Game Semantics Model for Security Protocols -- Communication -- Towards Dynamically Communicating Abstract Machines in the B Method -- Sweep-Line Analysis of TCP Connection Management -- 2/3 Alternating Simulation Between Interface Automata -- Development -- Formal Model-Driven Development of Communicating Systems -- Jahuel: A Formal Framework for Software Synthesis -- Modelling and Refinement of an On-Chip Communication Architecture -- Testing -- Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics -- Adaptive Random Testing by Bisection with Restriction -- Testing Real-Time Multi Input-Output Systems -- Verification -- Formal Verification of a Memory Model for C-Like Imperative Languages -- Symbolic Verification of Distributed Real-Time Systems with Complex Synchronizations -- An Improved Rule for While Loops in Deductive Program Verification -- Using Stålmarck?s Algorithm to Prove Inequalities -- Automatic Refinement Checking for B -- Slicing an Integrated Formal Method for Verification -- A Static Communication Elimination Algorithm for Distributed System Verification -- Incremental Verification of Owicki/Gries Proof Outlines Using PVS -- Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry -- Tools -- An Automated Approach to Specification-Based Program Inspection -- Visualizing and Simulating Semantic Web Services Ontologies -- A Model-to-Implementation Mapping Tool for Automated Model-Based GUI Testing -- ClawZ: Cost-Effective Formal Verification for Control Systems -- SVG Web Environment for Z Specification Language. 410 0$aLecture notes in computer science ;$v3785. 517 3 $a7th International Conference on Formal Engineering Methods 517 3 $aInternational Conference on Formal Engineering Methods 517 3 $aICFEM 2005 606 $aFormal methods (Computer science)$vCongresses 606 $aSoftware engineering$vCongresses 615 0$aFormal methods (Computer science) 615 0$aSoftware engineering 676 $a005.13/1 701 $aLau$b K.-K$g(Kung-Kiu),$f1953-$01759624 701 $aBanach$b Richard$01759625 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483536203321 996 $aFormal methods and software engineering$94198196 997 $aUNINA