04886nam 22006255 450 99646572970331620200704085922.010.1007/11576280(CKB)1000000000213336(SSID)ssj0000317704(PQKBManifestationID)11258695(PQKBTitleCode)TC0000317704(PQKBWorkID)10294160(PQKB)11401971(DE-He213)978-3-540-32250-4(MiAaPQ)EBC3067537(PPN)123098424(EXLCZ)99100000000021333620100410d2005 u| 0engurnn|008mamaatxtccrFormal Methods and Software Engineering[electronic resource] 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings /edited by Kung-Kiu Lau, Richard Banach1st ed. 2005.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2005.1 online resource (XIV, 502 p.) Programming and Software Engineering ;3785Bibliographic Level Mode of Issuance: MonographPrinted edition: 9783540297970 Includes bibliographical references and index.Invited 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.Programming and Software Engineering ;3785Software engineeringComputer logicProgramming languages (Electronic computers)Software Engineering/Programming and Operating Systemshttps://scigraph.springernature.com/ontologies/product-market-codes/I14002Software Engineeringhttps://scigraph.springernature.com/ontologies/product-market-codes/I14029Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XProgramming Languages, Compilers, Interpretershttps://scigraph.springernature.com/ontologies/product-market-codes/I14037Software engineering.Computer logic.Programming languages (Electronic computers).Software Engineering/Programming and Operating Systems.Software Engineering.Logics and Meanings of Programs.Programming Languages, Compilers, Interpreters.005.13/1Lau Kung-Kiuedthttp://id.loc.gov/vocabulary/relators/edtBanach Richardedthttp://id.loc.gov/vocabulary/relators/edtBOOK996465729703316Formal Methods and Software Engineering771999UNISA