Formal Methods and Software Engineering

1. Front Matter

   PDF

2. Invited Talks

   1. Towards a Signal Calculus for Event-Based Synchronous Languages

      • Yongxin Zhao, He Jifeng

      Pages 1-13

   2. Reasoning about Programs Using a Scientific Method

      • Peter W. O’Hearn

      Pages 14-14

   3. Poirot—A Concurrency Sleuth

      • Shaz Qadeer

      Pages 15-15

3. Formal Models

   1. Context-Based Behavioral Equivalence of Components in Self-Adaptive Systems

      • Narges Khakpour, Marjan Sirjani, Ursula Goltz

      Pages 16-32

   2. Towards a Practical Approach to Check UML/fUML Models Consistency Using CSP

      • Islam Abdelhalim, Steve Schneider, Helen Treharne

      Pages 33-48

   3. The Safety-Critical Java Mission Model: A Formal Account

      • Frank Zeyda, Ana Cavalcanti, Andy Wellings

      Pages 49-65

   4. Is There Evolution Before Birth? Deterioration Effects of Formal Z Specifications

      • Andreas Bollin

      Pages 66-81

   5. Asynchronous Communication in MSVL

      • Dapeng Mo, Xiaobing Wang, Zhenhua Duan

      Pages 82-97

4. Model Checking and Probability

   1. Verification of Orchestration Systems Using Compositional Partial Order Reduction

      • Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong

      Pages 98-114

   2. Domain-Driven Probabilistic Analysis of Programmable Logic Controllers

      • Hehua Zhang, Yu Jiang, William N. N. Hung, Xiaoyu Song, Ming Gu

      Pages 115-130

   3. Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications

      • João Martins, André Platzer, João Leite

      Pages 131-146

   4. PRTS: An Approach for Model Checking Probabilistic Real-Time Hierarchical Systems

      • Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li

      Pages 147-162

5. Specification and Development

   1. Integrating Prototyping into the SOFL Three-Step Modeling Approach

      • Fauziah binti Zainuddin, Shaoying Liu

      Pages 163-178

   2. A Deterministic Interpreter Simulating a Distributed Real Time System Using VDM

      • Kenneth Lausdahl, Peter Gorm Larsen, Nick Battle

      Pages 179-194

   3. On Fitting a Formal Method into Practice

      • Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge

      Pages 195-210

   4. A Formal Engineering Approach to High-Level Design of Situation Analysis Decision Support Systems

      • Roozbeh Farahbod, Vladimir Avram, Uwe Glässer, Adel Guitouni

      Pages 211-226

6. Security

   1. Conformance Checking of Dynamic Access Control Policies

      • David Power, Mark Slaymaker, Andrew Simpson

      Pages 227-242

   2. A Knowledge-Based Verification Method for Dynamic Access Control Policies

      • Masoud Koleini, Mark Ryan

      Pages 243-258

   3. Validation of Security-Design Models Using Z

      • Nafees Qamar, Yves Ledru, Akram Idani

      Pages 259-274

This book constitutes the refereed proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011, held in Durham, UK, October 2011. The 40 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 103 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on formal models; model checking and probability; specification and development; security; formal verification; cyber physical systems; event-B; verification, analysis and testing; refinement; as well as theorem proving and rewriting.

• automated reasoning
• constraint solving
• higher-order-logic
• probabilistic analysis
• timed automata
• algorithm analysis and problem complexity

• School of Computing, Teesside University, UK

  Shengchao Qin

• LMAM and Department of Informatics, School of Mathematical Sciences,, Peking University, China

  Zongyan Qiu

Policies and ethics