04870nam 22008175 450 991048476560332120251226200340.03-540-76650-210.1007/978-3-540-76650-6(CKB)1000000000490578(SSID)ssj0000317702(PQKBManifestationID)11258694(PQKBTitleCode)TC0000317702(PQKBWorkID)10294841(PQKB)10821892(DE-He213)978-3-540-76650-6(MiAaPQ)EBC3065436(MiAaPQ)EBC6512619(Au-PeEL)EBL6512619(OCoLC)191471094(PPN)123728940(MiAaPQ)EBC337063(BIP)32373979(BIP)17712365(EXLCZ)99100000000049057820100301d2007 u| 0engurnn#008mamaatxtccrFormal Methods and Software Engineering 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, Florida, USA, November 14-15, 2007, Proceedings /edited by Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie1st ed. 2007.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2007.1 online resource (VIII, 387 p.)Programming and Software Engineering,2945-9168 ;4789Bibliographic Level Mode of Issuance: Monograph3-540-76648-0 Includes bibliographical references and index.Invited Talks -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification.This book constitutes the refereed proceedings of the 9th International Conference on Formal Engineering Methods, ICFEM 2007, held in Boca Raton, Florida, USA, November 14-15, 2007. The 19 revised full papers together with two invited talks presented were carefully reviewed and selected from 38 submissions. The papers address all current issues in formal methods and their applications in software engineering. The papers are organized in topical sections.Programming and Software Engineering,2945-9168 ;4789Software engineeringComputer programmingComputer scienceCompilers (Computer programs)Software EngineeringProgramming TechniquesModels of ComputationComputer Science Logic and Foundations of ProgrammingCompilers and InterpretersSoftware engineering.Computer programming.Computer science.Compilers (Computer programs).Software Engineering.Programming Techniques.Models of Computation.Computer Science Logic and Foundations of Programming.Compilers and Interpreters.004.0151Hinchey Michael G(Michael Gerard),1969-Larrondo-Petrie María M.Butler Michael1967-MiAaPQMiAaPQMiAaPQBOOK9910484765603321Formal Methods and Software Engineering771999UNINA