Formal Methods: Foundations and Applications: 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings

✍ Scribed by John Rushby (auth.), Rohit Gheyi, David Naumann (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2012
• Tongue: English
• Leaves: 234
• Series: Lecture Notes in Computer Science 7498 Programming and Software Engineering
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

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 -

✦ Subjects

Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Programming Languages, Compilers, Interpreters; Management of Computing and Information Systems; Computer Science, general