Formal Methods: Foundations and Applications: 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings (Lecture Notes in Computer Science (7498))

This book constitutes the refereed proceedings of the 15th Brazilian Symposium on Formal Methods, SBMF 2012, held in Natal, Brazil, in September 2012; co-located with CBSoft 2012, the Third Brazilian Conference on Software: Theory and Practice. 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. Front Matter....Pages - The Versatile Synchronous Observer....Pages 1-1 Thirteen Years of Automated Code Analysis at Microsoft....Pages 2-2 Model Checking Propositional Deontic Temporal Logic via a μ -Calculus Characterization....Pages 3-18 An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting....Pages 19-34 Palytoxin Inhibits the Sodium-Potassium Pump – An Investigation of an Electrophysiological Model Using Probabilistic Model Checking....Pages 35-50 BETA: A B Based Testing Approach....Pages 51-66 A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications....Pages 67-82 Specification Patterns for Properties over Reachable States of Graph Grammars....Pages 83-98 Compositionality and Refinement in Model-Driven Engineering....Pages 99-114 Identifying Hardware Failures Systematically....Pages 115-130 Investigating Time Properties of Interrupt-Driven Programs....Pages 131-146 Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows....Pages 147-162 Composition of Model Transformations: A Categorical Framework....Pages 163-178 Verification Rules for Exception Handling in Eiffel....Pages 179-193 A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications....Pages 194-209 Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions....Pages 210-225 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