Formal Methods and Software Engineering

Inhaltsverzeichnis

• 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 theConformance 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.