Formal Methods and Software Engineering

1. Front Matter

   PDF

2. Keynote

   1. Lattices of Information for Security: Deterministic, Demonic, Probabilistic

      • Carroll C. Morgan

      Pages 1-3

3. Specification

   1. Algebraic Laws for Process Subtyping

      • José Dihego, Pedro Antonino, Augusto Sampaio

      Pages 4-19

   2. Boundness Issues in CCSL Specifications

      • Frédéric Mallet, Jean-Viven Millo

      Pages 20-35

   3. Mining Dataflow Sensitive Specifications

      • Zhiqiang Zuo, Siau-Cheng Khoo

      Pages 36-52

4. Proof

   1. A Proof Slicing Framework for Program Verification

      • Ton Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin

      Pages 53-69

   2. Formally Verified System Initialisation

      • Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway et al.

      Pages 70-85

   3. Verifying an Aircraft Proximity Characterization Method in Coq

      • Dongxi Liu, Neale L. Fulton, John Zic, Martin de Groot

      Pages 86-101

5. Testing

   1. Assisting Specification Refinement by Random Testing

      • Mengjun Li

      Pages 102-114

   2. Generation of Checking Sequences Using Identification Sets

      • Faimison Rodrigues Porto, Andre Takeshi Endo, Adenilso Simao

      Pages 115-130

   3. The Circus Testing Theory Revisited in Isabelle/HOL

      • Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, Burkhart Wolff

      Pages 131-147

6. Timed Systems

   1. A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification

      • Gustavo Carvalho, Augusto Sampaio, Alexandre Mota

      Pages 148-164

   2. Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts

      • Yanhong Huang, João F. Ferreira, Guanhua He, Shengchao Qin, Jifeng He

      Pages 165-181

   3. Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction

      • Yuanjie Si, Jun Sun, Yang Liu, Ting Wang

      Pages 182-198

7. Concurrency

   1. A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems

      • Étienne André, Benoît Barbot, Clément Démoulins, Lom Messan Hillah, Francis Hulin-Hubard, Fabrice Kordon et al.

      Pages 199-214

   2. A UTP Semantics for Communicating Processes with Shared Variables

      • Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, Shengchao Qin

      Pages 215-230

   3. Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions

      • Duy-Khanh Le, Wei-Ngan Chin, Yong-Meng Teo

      Pages 231-248

8. SysML/MDD

   1. Formal Models of SysML Blocks

      • Alvaro Miyazawa, Lucas Lima, Ana Cavalcanti

      Pages 249-264

   2. Towards a Process Algebra Framework for Supporting Behavioural Consistency and Requirements Traceability in SysML

      • Jaco Jacobs, Andrew Simpson

      Pages 265-280

   3. Translation from Workflow Nets to MSVL

      • Ya Shi, Zhenhua Duan, Cong Tian

      Pages 281-296

This book constitutes the refereed proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, held in Queenstown, New Zealand, in October/November 2013. The 28 revised full papers together with 2 keynote speeches presented were carefully reviewed and selected from 88 submissions. The topics covered are abstraction and refinement, formal specification and modeling, program analysis, software verification, formal methods for software safety, security, reliability and dependability, tool development, integration and experiments involving verified systems, formal methods used in certifying products under international standards, and formal model-based development and code generation.

• concurrent systems
• denotational semantics
• model checking
• program refinement
• symbolic computations
• algorithm analysis and problem complexity

• School of Engineering and Computer Science, Victoria University of Wellington, Wellington, New Zealand

  Lindsay Groves

• Department of Computer Science, The University of Auckland, Auckland, New Zealand

  Jing Sun

Policies and ethics