Software Engineering and Formal Methods

1. Front Matter

   PDF

2. Real-Time Systems

   1. Verifying MARTE/CCSL Mode Behaviors Using UPPAAL

      • Jagadish Suryadevara, Cristina Seceleanu, Frédéric Mallet, Paul Pettersson

      Pages 1-15

   2. A Transformation Approach for Multiform Time Requirements

      • Nadia Menad, Philippe Dhaussy

      Pages 16-30

   3. Real-Time Migration Properties of rTiMo Verified in Uppaal

      • Bogdan Aman, Gabriel Ciobanu

      Pages 31-45

3. Verification 1

   1. A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP

      • Marcel Vinicius Medeiros Oliveira, Ivan Soares De Medeiros Júnior, Jim Woodcock

      Pages 46-60

   2. From Extraction of Logical Specifications to Deduction-Based Formal Verification of Requirements Models

      • Radosław Klimek

      Pages 61-75

   3. Model Checking of Security-Critical Applications in a Model-Driven Approach

      • Marian Borek, Nina Moebius, Kurt Stenzel, Wolfgang Reif

      Pages 76-90

4. Verification 2

   1. Lifting Verification Results for Preemption Statements

      • Manuel Gesell, Andreas Morgenstern, Klaus Schneider

      Pages 91-105

   2. Rule-Level Verification of Graph Transformations for Invariants Based on Edges’ Transitive Closure

      • Christian Percebois, Martin Strecker, Hanh Nhi Tran

      Pages 106-121

   3. Sound Symbolic Linking in the Presence of Preprocessing

      • Gijs Vanspauwen, Bart Jacobs

      Pages 122-136

5. Types and Inference

   1. Inferring Physical Units in B Models

      • Sebastian Krings, Michael Leuschel

      Pages 137-151

   2. A Tool for Behaviour-Based Discovery of Approximately Matching Web Services

      • Mahdi Sargolzaei, Francesco Santini, Farhad Arbab, Hamideh Afsarmanesh

      Pages 152-166

   3. A Type System for Components

      • Ornela Dardha, Elena Giachino, Michaël Lienhardt

      Pages 167-181

6. Static Analysis

   1. Early Fault Detection in DSLs Using SMT Solving and Automated Debugging

      • Sarmen Keshishzadeh, Arjan J. Mooij, Mohammad Reza Mousavi

      Pages 182-196

   2. Static Detection of Implementation Errors Using Formal Code Specification

      • Iman Saleh, Gregory Kulczycki, M. Brian Blake, Yi Wei

      Pages 197-211

   3. Compositional Static Analysis for Implicit Join Synchronization in a Transactional Setting

      • Thi Mai Thuong Tran, Martin Steffen, Hoang Truong

      Pages 212-228

7. Testing and Runtime Verification

   1. {log} as a Test Case Generator for the Test Template Framework

      • Maximiliano Cristiá, Gianfranco Rossi, Claudia Frydman

      Pages 229-243

   2. Zero Overhead Runtime Monitoring

      • Daniel Wonisch, Alexander Schremmer, Heike Wehrheim

      Pages 244-258

   3. Run-Time Verification of Coboxes

      • Frank S. de Boer, Stijn de Gouw, Peter Y. H. Wong

      Pages 259-273

8. Synthesis and Transformation

   1. Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning

      • Amel Bennaceur, Chris Chilton, Malte Isberner, Bengt Jonsson

      Pages 274-288

This book constitutes the refereed proceedings of the11th International Conference on Software Engineering and Formal Methods, SEFM 2013, held in Madrid, Spain, in September 2013. The 21 full papers included in this volume were carefully reviewed and selected from 58 submissions. They are organized in topical section on real-time systems, verification, types and inference, static analysis, testing and runtime verification, and synthesis and transformation.

• model-checking
• ontology
• requirements engineering
• temporal logic
• verification

• School of Information Systems, Computing and Mathematics, Brunel University, Uxbridge, UK

  Robert M. Hierons

• Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, Madrid, Spain

  Mercedes G. Merayo

• Dipartimento di Scienze dell’Informazione, Università di Bologna, Bologna, Italy

  Mario Bravetti

Policies and ethics