Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings

Front Matter....Pages -
Seamless Model Driven Systems Engineering Based on Formal Models....Pages 1-19
Compositional Verification of Input-Output Conformance via CSP Refinement Checking....Pages 20-48
Symbolic Query Exploration....Pages 49-68
Event Listener Analysis and Symbolic Execution for Testing GUI Applications....Pages 69-87
An Empirical Study of Structural Constraint Solving Techniques....Pages 88-106
Improving Automatic Verification of Security Protocols with XOR....Pages 107-126
Modeling and Verification of Privacy Enhancing Protocols....Pages 127-146
Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support....Pages 147-166
Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing....Pages 167-185
A Statistical Approach to Test Stochastic and Probabilistic Systems....Pages 186-205
Qualitative Action Systems....Pages 206-225
RAFFS: Model Checking a Robust Abstract Flash File Store....Pages 226-245
European Train Control System: A Case Study in Formal Verification....Pages 246-265
Development of Security Software: A High Assurance Methodology....Pages 266-285
Bounded Semantics of CTL and SAT-Based Verification....Pages 286-305
Graded-CTL: Satisfiability and Symbolic Model Checking....Pages 306-325
Approximate Model Checking of PCTL Involving Unbounded Path Properties....Pages 326-346
A Graph-Based Operational Semantics of OO Programs....Pages 347-366
Modeling and Analysis of Thread-Pools in an Industrial Communication Platform....Pages 367-386
A Verification System for Distributed Objects with Asynchronous Method Calls....Pages 387-406
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties....Pages 407-425
Scalable Multi-core Model Checking Fairness Enhanced Systems....Pages 426-445
Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language....Pages 446-465
Supporting Reuse of Event-B Developments through Generic Instantiation....Pages 466-484
A Lazy Unbounded Model Checker for Event-B ....Pages 485-503
Proof Assisted Model Checking for B....Pages 504-520
Machine-Checked Sequencer for Critical Embedded Code Generator....Pages 521-540
Implementing a Direct Method for Certificate Translation....Pages 541-560
Algorithmic Verification with Multiple and Nested Parameters....Pages 561-580
Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction....Pages 581-600
Modal Systems: Specification, Refinement and Realisation....Pages 601-619
Refinement-Preserving Co-evolution....Pages 620-638
Circular Coinduction with Special Contexts....Pages 639-659
The VSE Refinement Method in Hets ....Pages 660-678
A Compositional Approach on Modal Specifications for Timed Systems....Pages 679-697
An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata....Pages 698-716
Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude....Pages 717-736
Specifying and Verifying Business Processes Using PPML....Pages 737-756
Back Matter....Pages -