Formal Methods and Software Engineering

5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings

AvJin Song Dong,Jim Woodcock

Häftad, Engelska, 2003

Del i serien Lecture Notes in Computer Science

1 095 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

This book constitutes the refereed proceedings of the 5th International Conference on Formal Engineering Methods, ICFEM 2003, held in Singapore in November 2003.The 34 revised full papers presented together with 3 invited contributions were carefully reviewed and selected from 91 submissions. The papers are organized in topical sections on testing and validation, state diagrams, PVS/HOL, refinement, hybrid systems, Z/Object-Z, Petri nets, timed automata, system modelling and checking, and semantics and synthesis.

Produktinformation

Utgivningsdatum:2003-10-27
Mått:155 x 235 x 38 mm
Vikt:1 042 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:682
Upplaga:2003
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783540204619

Utforska kategorier

Programvaruutveckling inom Data och IT

Innehållsförteckning

Invited Talks.- Programs as Paths: An Approach to Timing Constraint Analysis.- Model Based Code Verification.- Adding Formalism to Methods or Where and When Will Industry Use Formal Reasoning?.- Testing and Validation.- Using Formal Methods to Serialize Synchronization Events.- An AMBA-ARM7 Formal Verification Platform.- Formalization, Testing and Execution of a Use Case Diagram.- Service-Based Systems Engineering: Consistent Combination of Services.- State Diagrams.- Using State Diagrams to Describe Concurrent Behaviour.- The Equivalence of Statecharts.- Generic Interacting State Machines and Their Instantiation with Dynamic Features.- PVS/HOL.- Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language.- Formalising an Integrated Language in PVS.- Refinement.- Modeling SystemC Fixed-Point Arithmetic in HOL.- Adding Action Refinement to Stochastic True Concurrency Models.- Incremental Derivation of Abstraction Relations for Data Refinement.- Comparison of Data and Process Refinement.- Compilation by Refinement for a Practical Assembly Language.- Hybrid Systems.- Java Card Code Generation from B Specifications.- Efficient Path Finding with the Sweep-Line Method Using External Storage.- Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates.- Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures.- Z/Object-Z.- A Z Based Approach to Verifying Security Protocols.- A Refinement Tool for Z.- The Common Semantic Constructs of XML Family.- Petri Nets.- Controller Synthesis for Object Petri Nets.- Towards a Workflow Model of Real-Time Cooperative Systems.- New Developments in Closed-Form Computation for GSPN Aggregation.- Timed Automata.- On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata.- Analyzing the Redesign of a Distributed Lift System in UPPAAL.- Verification of Timeliness QoS Properties in Multimedia Systems.- System Modeling and Checking.- A Calculus for Set-Based Program Development.- Compositional Verification of a Switch Fabric from Nortel Networks.- Constraint-Based Model Checking of Data-Independent Systems.- A Formal Model for the Block Device Subsystem of the Linux Kernel.- Semantics and Synthesis.- A Mathematical Framework for Safecharts.- A Relational Model for Formal Object-Oriented Requirement Analysis in UML.- From Specification to Hardware Device: A Synthesis Algorithm.