Formal Methods: Foundations and Applications 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Oliveira, Marcel Vinícius Medeiros (Επιμελητής έκδοσης), Woodcock, Jim (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2009.
• Σειρά: Lecture Notes in Computer Science, 5902
• Θέματα: Computer science.; Software engineering.; Computer programming.; Programming languages (Electronic computers).; Computers.; Computer logic.; Computer Science.; Software Engineering/Programming and Operating Systems.; Programming Languages, Compilers, Interpreters.; Theory of Computation.; Software Engineering.; Logics and Meanings of Programs.; Programming Techniques.

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 paper...

Πίνακας περιεχομένων:

• Speeding Up Simulation of SystemC Using Model Checking
• Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering
• Satisfiability Modulo Theories: An Appetizer
• Interruption Testing of Reactive Systems
• Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS
• Concurrent Models of Flash Memory Device Behaviour
• Corecursive Algebras: A Study of General Structured Corecursion
• Formalizing FreeRTOS: First Steps
• A Mechanized Strategy for Safe Abstraction of CSP Specifications
• Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
• An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model
• Towards Safe Design of Synchronous Bus Protocols in Event-B
• Mechanising Data-Types for Kernel Design in Z
• A Complete Set of Object Modeling Laws for Alloy
• Undecidability Results for Distributed Probabilistic Systems
• Formalisation and Analysis of Objects as CSP Processes
• Concolic Testing of the Multi-sector Read Operation for Flash Memory File System
• Low-Level Code Verification Based on CSP Models
• Formal Modelling of a Microcontroller Instruction Set in B
• Defining Behaviours by Quasi-finality
• Verifying Compiled File System Code
• Reasoning about General Quantum Programs over Mixed States
• A Simple and General Theoretical Account for Abstract Types.