Sciweavers

ASM
2008
ASM
13 years 9 months ago
Modelling Attacker's Knowledge for Cascade Cryptographic Protocols
We address the proof-based development of cryptographic protocols satisfying security properties. Communication channels are supposed to be unsafe. Analysing cryptographic protocol...
Nazim Benassa
ASM
2008
ASM
13 years 9 months ago
The Composition of Event-B Models
The transition from classical B [2] to the Event-B language and method [3] has seen the removal of some forms of model structuring and composition, with the intention of reinventin...
Michael Poppleton
ASM
2008
ASM
13 years 9 months ago
FDIR Architectures for Autonomous Spacecraft: Specification and Assessment with Event-B
On-board Fault Detection, Isolation and Recovery (FDIR) systems are considered to ensure the safety and to increase the autonomy of spacecrafts. They shall be carefully designed an...
Jean-Charles Chaudemar, Charles Castel, Christel S...
ASM
2008
ASM
13 years 9 months ago
A Roadmap for the Rodin Toolset
Jean-Raymond Abrial, Michael J. Butler, Stefan Hal...
ASM
2008
ASM
13 years 9 months ago
Model Based Refinement and the Tools of Tomorrow
The ingredients of typical model based development via refinement are re-examined, and some well known frameworks are reviewed in that light, drawing out commonalities and differen...
Richard Banach
ASM
2008
ASM
13 years 9 months ago
The High Road to Formal Validation:
Abstract. In this paper we examine the difference between model checking high-level and low-level models. In particular, we compare the ProB model checker for the B-method and the ...
Michael Leuschel
ASM
2008
ASM
13 years 9 months ago
UML-B: A Plug-in for the Event-B Tool Set
UML-B provides a graphical front end for Event-B. It adds support for class-oriented and state machine modelling. UML-B is similar to UML but has its own meta-model. UML-B provides...
Colin F. Snook, Michael J. Butler
ASM
2008
ASM
13 years 9 months ago
From ABZ to Cryptography
Eerke A. Boiten
ASM
2008
ASM
13 years 9 months ago
On the Purpose of Event-B Proof Obligations
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges o...
Stefan Hallerstede
ASM
2008
ASM
13 years 9 months ago
Using EventB to Create a Virtual Machine Instruction Set Architecture
A Virtual Machine (VM) is a program running on a conventional microprocessor that emulates the binary instruction set, registers, and memory space of an idealized computing machine...
Stephen Wright