Titlebook: Integrated Formal Methods; 9th International Co John Derrick,Stefania Gnesi,Helen Treharne Conference proceedings 2012 Springer-Verlag Berl

Lice692

LIKEN

Early Fault Detection in Industry Using Models at Various Abstraction Levels,ts phases. To this end we have made additional formal models, both for the requirements and for the early designs at various abstraction levels. We have analysed these models using simulation and interactive visualization, and we have compared them using refinement checking.

deriver

HUMID

white-matter

Formal Verification of Compiler Transformations on Polychronous Equations,ves the correctness of this running. The compiler will continue its work if and only if the correctness is proved positively. In this paper, the highly optimizing, industrial compiler from the synchronous language SIGNAL to C is addressed.

废止

Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems,orrect development in Event-B, we need to devise a way of integrating these formalisms. In this paper we propose a refinement-based translation from Event-B to rv-IS, exemplified with a file transfer protocol modelled in both formalisms.

commune

Conference proceedings 2012012. The 20 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 59 submissions. The papers cover the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, proof frameworks, refinement, verification, timed sy

犬儒主义者

ANN

Mechanized Extraction of Topology Anti-patterns in Wireless Networks,called anti-patterns, of small size. We propose techniques to find such anti-patterns using a combination of model-checking and automated debugging. We apply the proposed technique on two well-known protocols for wireless sensor networks and show that the techniques indeed find the root causes in terms of canonical topologies featuring the fault.

枪支

A UTP Semantics of pGCL as a Homogeneous Relation,after-states: these predicates capture the same information as the models traditionally used to give semantics to pGCL; in addition our formulation allows us to define a generic choice construct, that covers conditional, probabilistic and non-deterministic choice. As an example we study the Monty Hall game in this framework.