Formal methods and software engineering : 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006 : proceedings /
Formal methods and software engineering : 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006 : proceedings /
8th International Conference on Formal Engineering Methods Eighth International Conference on Formal Engineering Methods International Conference on Formal Engineering Methods ICFEM 2006
Zhiming Liu, Jifeng He (eds.).
- Berlin ; New York : Springer, ©2006.
- 1 online resource (xii, 778 pages) : illustrations
- Lecture notes in computer science, 4260 0302-9743 ; .
- Lecture notes in computer science ; 4260. .
Includes bibliographical references and index.
Keynote Talks -- Program Verification Through Computer Algebra -- JML's Rich, Inherited Specifications for Behavioral Subtypes -- Three Perspectives in Formal Engineering -- Specification and Verification -- A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces -- Applying Timed Interval Calculus to Simulink Diagrams -- Reducing Model Checking of the Few to the One -- Induction-Guided Falsification -- Verifying? Models of Industrial Systems with Spin -- Stateful Dynamic Partial-Order Reduction -- Internetware and Web-Based Systems -- User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition -- Environment Ontology-Based Capability Specification for Web Service Discovery -- Scenario-Based Component Behavior Derivation -- Verification of Computation Orchestration Via Timed Automata -- Towards the Semantics for Web Service Choreography Description Language -- Type Checking Choreography Description Language -- Concurrent, Communicating, Timing and Probabilistic Systems -- Formalising Progress Properties of Non-blocking Programs -- Towards a Fully Generic Theory of Data -- Verifying Statemate Statecharts Using CSP and FDR -- A Reasoning Method for Timed CSP Based on Constraint Solving -- Mapping RT-LOTOS Specifications into Time Petri Nets -- Reasoning Algebraically About Probabilistic Loops -- Object and Component Orientation -- Formal Verification of the Heap Manager of an Operating System Using Separation Logic -- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs -- Model Checking Dynamic UML Consistency -- Testing and Model Checking -- Conditions for Avoiding Controllability Problems in Distributed Testing -- Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm -- Checking the Conformance of Java Classes Against Algebraic Specifications -- Incremental Slicing -- Assume-Guarantee Software Verification Based on Game Semantics -- Optimized Execution of Deterministic Blocks in Java PathFinder -- Tools -- A Tool for a Formal Pattern Modeling Language -- An Open Extensible Tool Environment for Event-B -- Tool for Translating Simulink Models into Input Language of a Model Checker -- Fault-Tolerance and Security -- Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices -- A Language for Modeling Network Availability -- Multi-process Systems Analysis Using Event B: Application to Group Communication Systems -- Specification and Refinement -- Issues in Implementing a Model Checker for Z -- Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking -- Discovering Likely Method Specifications -- Time Aware Modelling and Analysis of Multiclocked VLSI Systems -- SALT--Structured Assertion Language for Temporal Logic.
Available to OhioLINK libraries.
9783540474623 3540474625 3540474609 9783540474609
978-3-540-47460-9 Springer http://www.springerlink.com
981257682 DE-101
Formal methods (Computer science)--Congresses.
Software engineering--Congresses.
Méthodes formelles (Informatique)--Congrès.
Génie logiciel--Congrès.
Informatique.
Formal methods (Computer science)
Software engineering.
computerwetenschappen computer sciences programmeertalen programming languages software engineering Information and Communication Technology (General) Informatie- en communicatietechnologie (algemeen)
Congress
Conference papers and proceedings.
Conference papers and proceedings.
Actes de congrès.
QA76.9.F67 / I5788 2006eb
005.13/1
Includes bibliographical references and index.
Keynote Talks -- Program Verification Through Computer Algebra -- JML's Rich, Inherited Specifications for Behavioral Subtypes -- Three Perspectives in Formal Engineering -- Specification and Verification -- A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces -- Applying Timed Interval Calculus to Simulink Diagrams -- Reducing Model Checking of the Few to the One -- Induction-Guided Falsification -- Verifying? Models of Industrial Systems with Spin -- Stateful Dynamic Partial-Order Reduction -- Internetware and Web-Based Systems -- User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition -- Environment Ontology-Based Capability Specification for Web Service Discovery -- Scenario-Based Component Behavior Derivation -- Verification of Computation Orchestration Via Timed Automata -- Towards the Semantics for Web Service Choreography Description Language -- Type Checking Choreography Description Language -- Concurrent, Communicating, Timing and Probabilistic Systems -- Formalising Progress Properties of Non-blocking Programs -- Towards a Fully Generic Theory of Data -- Verifying Statemate Statecharts Using CSP and FDR -- A Reasoning Method for Timed CSP Based on Constraint Solving -- Mapping RT-LOTOS Specifications into Time Petri Nets -- Reasoning Algebraically About Probabilistic Loops -- Object and Component Orientation -- Formal Verification of the Heap Manager of an Operating System Using Separation Logic -- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs -- Model Checking Dynamic UML Consistency -- Testing and Model Checking -- Conditions for Avoiding Controllability Problems in Distributed Testing -- Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm -- Checking the Conformance of Java Classes Against Algebraic Specifications -- Incremental Slicing -- Assume-Guarantee Software Verification Based on Game Semantics -- Optimized Execution of Deterministic Blocks in Java PathFinder -- Tools -- A Tool for a Formal Pattern Modeling Language -- An Open Extensible Tool Environment for Event-B -- Tool for Translating Simulink Models into Input Language of a Model Checker -- Fault-Tolerance and Security -- Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices -- A Language for Modeling Network Availability -- Multi-process Systems Analysis Using Event B: Application to Group Communication Systems -- Specification and Refinement -- Issues in Implementing a Model Checker for Z -- Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking -- Discovering Likely Method Specifications -- Time Aware Modelling and Analysis of Multiclocked VLSI Systems -- SALT--Structured Assertion Language for Temporal Logic.
Available to OhioLINK libraries.
9783540474623 3540474625 3540474609 9783540474609
978-3-540-47460-9 Springer http://www.springerlink.com
981257682 DE-101
Formal methods (Computer science)--Congresses.
Software engineering--Congresses.
Méthodes formelles (Informatique)--Congrès.
Génie logiciel--Congrès.
Informatique.
Formal methods (Computer science)
Software engineering.
computerwetenschappen computer sciences programmeertalen programming languages software engineering Information and Communication Technology (General) Informatie- en communicatietechnologie (algemeen)
Congress
Conference papers and proceedings.
Conference papers and proceedings.
Actes de congrès.
QA76.9.F67 / I5788 2006eb
005.13/1