Formal Methods and Software Engineering (eBook)

Invited Papers.- Seamless Model Driven Systems Engineering Based on Formal Models.- Compositional Verification of Input-Output Conformance via CSP Refinement Checking.- Testing I.- Symbolic Query Exploration.- Event Listener Analysis and Symbolic Execution for Testing GUI Applications.- An Empirical Study of Structural Constraint Solving Techniques.- Protocols.- Improving Automatic Verification of Security Protocols with XOR.- Modeling and Verification of Privacy Enhancing Protocols.- Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support.- Testing II.- Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing.- A Statistical Approach to Test Stochastic and Probabilistic Systems.- Qualitative Action Systems.- Verification.- RAFFS: Model Checking a Robust Abstract Flash File Store.- European Train Control System: A Case Study in Formal Verification.- Development of Security Software: A High Assurance Methodology.- Model Checking I.- Bounded Semantics of CTL and SAT-Based Verification.- Graded-CTL: Satisfiability and Symbolic Model Checking.- Approximate Model Checking of PCTL Involving Unbounded Path Properties.- Object-Orientation.- A Graph-Based Operational Semantics of OO Programs.- Modeling and Analysis of Thread-Pools in an Industrial Communication Platform.- A Verification System for Distributed Objects with Asynchronous Method Calls.- Model checking II.- A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.- Scalable Multi-core Model Checking Fairness Enhanced Systems.- Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language.- Event-B.- Supporting Reuse of Event-B Developments through Generic Instantiation.- A Lazy Unbounded Model Checker for Event-B.- Proof Assisted Model Checking for B.- Compilation.- Machine-Checked Sequencer for Critical Embedded Code Generator.- Implementing a Direct Method for Certificate Translation.- Process Algebra.- Algorithmic Verification with Multiple and Nested Parameters.- Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction.- Refinement.- Modal Systems: Specification, Refinement and Realisation.- Refinement-Preserving Co-evolution.- Algebraic Specifications.- Circular Coinduction with Special Contexts.- The VSE Refinement Method in Hets.- Real-Time Systems.- A Compositional Approach on Modal Specifications for Timed Systems.- An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata.- Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude.- Specifying and Verifying Business Processes Using PPML.