Formal Methods and Software Engineering

1. Front Matter

   PDF

2. Invited Papers

   1. Seamless Model Driven Systems Engineering Based on Formal Models

      • Manfred Broy

      Pages 1-19

   2. Compositional Verification of Input-Output Conformance via CSP Refinement Checking

      • Augusto Sampaio, Sidney Nogueira, Alexandre Mota

      Pages 20-48

3. Testing I

   1. Symbolic Query Exploration

      • Margus Veanes, Pavel Grigorenko, Peli de Halleux, Nikolai Tillmann

      Pages 49-68

   2. Event Listener Analysis and Symbolic Execution for Testing GUI Applications

      • Svetoslav Ganov, Chip Killmar, Sarfraz Khurshid, Dewayne E. Perry

      Pages 69-87

   3. An Empirical Study of Structural Constraint Solving Techniques

      • Junaid Haroon Siddiqui, Sarfraz Khurshid

      Pages 88-106

4. Protocols

   1. Improving Automatic Verification of Security Protocols with XOR

      • Xihui Chen, Ton van Deursen, Jun Pang

      Pages 107-126

   2. Modeling and Verification of Privacy Enhancing Protocols

      • Suriadi Suriadi, Chun Ouyang, Jason Smith, Ernest Foo

      Pages 127-146

   3. Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support

      • Péter Bokor, Marco Serafini, Neeraj Suri, Helmut Veith

      Pages 147-166

5. Testing II

   1. Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing

      • Maximiliano Cristiá, Pablo Rodríguez Monetti

      Pages 167-185

   2. A Statistical Approach to Test Stochastic and Probabilistic Systems

      • Mercedes G. Merayo, Iksoon Hwang, Manuel Núñez, Ana Cavalli

      Pages 186-205

   3. Qualitative Action Systems

      • Bernhard K. Aichernig, Harald Brandl, Willibald Krenn

      Pages 206-225

6. Verification

   1. RAFFS: Model Checking a Robust Abstract Flash File Store

      • Paul Taverne, C. (Kees) Pronk

      Pages 226-245

   2. European Train Control System: A Case Study in Formal Verification

      • André Platzer, Jan-David Quesel

      Pages 246-265

   3. Development of Security Software: A High Assurance Methodology

      • David Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas Wagner, Michael Whalen

      Pages 266-285

7. Model Checking I

   1. Bounded Semantics of CTL and SAT-Based Verification

      • Wenhui Zhang

      Pages 286-305

   2. Graded-CTL: Satisfiability and Symbolic Model Checking

      • Alessandro Ferrante, Margherita Napoli, Mimmo Parente

      Pages 306-325

   3. Approximate Model Checking of PCTL Involving Unbounded Path Properties

      • Samik Basu, Arka P. Ghosh, Ru He

      Pages 326-346

8. Object-Orientation

   1. A Graph-Based Operational Semantics of OO Programs

      • Wei Ke, Zhiming Liu, Shuling Wang, Liang Zhao

      Pages 347-366

   2. Modeling and Analysis of Thread-Pools in an Industrial Communication Platform

      • Frank S. de Boer, Immo Grabe, Mohammad Mahdi Jaghoori, Andries Stam, Wang Yi

      Pages 367-386

Formal methods for development of computer systems have been extensively studied over the years. A range of semantic theories, speci?cation languages, design techniques, and veri?cation methods and tools have been developed and applied to the construction of programs used in critical applications. The ch- lenge now is to scale up formal methods and integrate them into engineering - velopment processes for the correct and e?cient construction and maintenance of computer systems in general. This requires us to improve the state of the art on approaches and techniques for integration of formal methods into industrial engineering practice, including new and emerging practice. The now long-established series of International Conferences on Formal - gineering Methods brings together those interested in the application of formal engineering methods to computer systems. Researchers and practitioners, from industry, academia, and government, are encouraged to attend and to help - vance the state of the art. This volume contains the papers presented at ICFEM 2009, the 11th International Conference on Formal Engineering Methods, held during December 9–11, in Rio de Janeiro, Brazil.

• B-Method
• CSP
• Coq
• certification
• dependable systems
• design patterns
• event-B
• fault tolerance
• formal methods
• formal software development
• formal specification
• formal verification
• hybrid systems
• software engineering
• verification

• Coordenadora da Engenharia de Computação, Diretora de Publicações da SBC, Depto. Informática, ontifícia Universidade Católica do Rio de Janeiro, ,, Rio de Jan,  

  Karin Breitman

• Department of Computer Science, University of York, ,, York, UK,

  Ana Cavalcanti

Policies and ethics