Paper Info
Title
How to Drive a B Machine
Abstract
The B-Method is a state-based formal method that describes behaviour in terms of MACHINES whose states change under OPERATIONS. The process algebra CSP is an event-based formalism that enables descriptions of patterns of system behaviour. We present a combination of the two views where a CSP process acts as a control executive and its events simply drive corresponding OPERATIONS. We define consistency between the two views in terms of existing semantic models. We identify proof conditions which are strong enough to ensure consistency and thus guarantee safety and liveness properties.
Year
Venue
Keywords
2000
ZB
corresponding operations,process algebra csp,b machine,system behaviour,state-based formal method,csp process act,semantic model,event-based formalism,control executive,liveness property,proof condition,process algebra,b method,formal method
Field
DocType
ISBN
Programming calculi,Computer science,Theoretical computer science,B-Method,Artificial intelligence,Formal methods,Formalism (philosophy),Process calculus,Abstract machine,Distributed computing,Liveness
Conference
3-540-67944-8
Citations 
PageRank 
References 
20
1.59
4
Authors
2
Name
Order
Citations
PageRank
Helen Treharne139036.94
Steve Schneider232326.65