| 10:00-10:05 | Introduction from the Chairs |
| 10:05-11:05 | Invited Talk (1) Stupid Tool Tricks for Smart Model Based Design Mark Lawford |
| 11:05-11:20 | Coffee Break |
| 11:20-12:50 | Technical Talks (1) ProRef: An Automatic Authentication Protocol Refinement Tool for Extracting Formal Models Quanqi Ye, Guangdong Bai, Naipeng Dong and Jin Song Dong Modeling Requirements for Quantitative Consistency Analysis and Automatic Test Case Generation Tom Bienmüller, Tino Teige, Andreas Eggers and Matthias Stasch Tool Support for Model-Based Database Design with Event-B Ahmed Al-Brashdi, Michael Butler, Abdolbaghi Rezazadeh and Colin Snook |
| 12:50-13:50 | Lunch |
| 13:50-14:50 | Invited Talk (2) Assured and Correct Dynamic Update of Controllers Kenji Tei |
| 14:50-15:50 | Technical Talks (2) PAndA^2: Analyzing Permission Use and Interplay in Android Apps (Tool Paper) Manuel Toews, Marie-Christine Jakobs and Felix Pauck A Formal Approach to Use Case Driven Testing Rajiv Murali, Andrew Ireland and Gudmund Grov |
| 15:50-16:20 | Coffee Break |
| 16:20-16:50 | Invited Industrial Presentation A Trial Application of B Method for an Embedded Device by Constructing B Model via UML Daichi Mizuguchi |
| 16:50-17:40 | Invited Technical Talk Safety Kernel for Control Systems DesignAlexei Iliasov |
| 17:40-18:00 | Discussion and Closing |
Stupid Tool Tricks for Smart Model Based Design
Mark Lawford, McMaster Centre for Software Certification / McMaster University
Formal methods tools can be used to detect and prevent errors so researchers assume that industry will use them. We are often frustrated when we see industrial projects where tools could have been used to detect or prevent errors in the final product. Researchers often fail to realize that there is a significant gap between a potentially useful tool and its use in a standards compliant, commercially viable, development process. In this talk I take a look at seemingly mundane industrial requirements - qualification (certification) of tools for use in standards compliant development process for general safety (IEC 61508), Automotive (ISO 26262) and Avionics (DO-178C), Model Based Design coding guidelines compliance, standards compliance documentation generation and integration with existing industry partner development processes. For each of these topics I show how “stupid tool tricks” can be used to not only increase adoption of academic methods and tools, but also lead to interesting research questions with industry relevant results.
Assured and Correct Dynamic Update of Controllers
Kenji Tei, National Institute of Informatics, Japan
In many application domains, continuous operation is a desirable attribute for software-intensive systems. As the environment or system requirements change, so the system should change and adapt without stopping or unduly disturbing its operation. There is, therefore, a need for sound engineering techniques that can cope with dynamic change. In this keynote, I will address the problem of dynamic update of controllers in reactive systems when the specification (environment assumptions, requirements and interface) of the current system changes. I will present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur. Indeed, using controller synthesis I will show how to automatically build a controller that guarantees both progress towards update and safe update. Seven case studies have been implemented to validate the approach.
A Trial Application of B Method for an Embedded Device by Constructing B Model via UML
Daichi Mizuguchi, Atelier Corporation
We are trying to apply B mothod for the development of embedded software for a safety-critical sensor device. We report our methodology, in which B models are constructed based on UML, and our outcomes.