Formal methods : foundations and applications ; 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 ; revised selected papers

This book constitutes the thoroughly refereed post-conference proceedings of the 12th Brazilian Symposium on Formal Methods, SBMF 2009, held in Gramado, Brazil, in August 2009 -- co-located with SAST 2009, the Brazilian Workshop on Systematic and Automated Software Testing. The 20 revised full papers presented together with 3 invited papers were carefully selected from numerous submissions during two rounds of reviewing and improvement. The papers are devoted to the dissemination of the development and use of formal methods for the design and verification of computational systems. The symposium provided an opportunity for researchers with a broad range of interests in formal methods for developing computing systems and software to discuss recent developments in this field. Front Matter....Pages - Speeding Up Simulation of SystemC Using Model Checking....Pages 1-16 Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering....Pages 17-22 Satisfiability Modulo Theories: An Appetizer....Pages 23-36 Interruption Testing of Reactive Systems....Pages 37-53 Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS....Pages 54-69 Concurrent Models of Flash Memory Device Behaviour....Pages 70-83 Corecursive Algebras: A Study of General Structured Corecursion....Pages 84-100 Formalizing FreeRTOS: First Steps....Pages 101-117 A Mechanized Strategy for Safe Abstraction of CSP Specifications....Pages 118-133 Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B....Pages 134-152 An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model....Pages 153-169 Towards Safe Design of Synchronous Bus Protocols in Event-B....Pages 170-185 Mechanising Data-Types for Kernel Design in Z....Pages 186-203 A Complete Set of Object Modeling Laws for Alloy....Pages 204-219 Undecidability Results for Distributed Probabilistic Systems....Pages 220-235 Formalisation and Analysis of Objects as CSP Processes....Pages 236-250 Concolic Testing of the Multi-sector Read Operation for Flash Memory File System....Pages 251-265 Low-Level Code Verification Based on CSP Models....Pages 266-281 Formal Modelling of a Microcontroller Instruction Set in B....Pages 282-289 Defining Behaviours by Quasi-finality....Pages 290-305 Verifying Compiled File System Code....Pages 306-320 Reasoning about General Quantum Programs over Mixed States....Pages 321-335 A Simple and General Theoretical Account for Abstract Types....Pages 336-349 Back Matter....Pages - This book constitutes the refereed proceedings of the 16th Brazilian Symposium on Formal Methods, SBMF 2013, held in Brasilia, Brazil, in September/October 2013. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains