next up previous
Next: Family and friends Up: Work Previous: Work

Whats new and interesting!

Using a common bridge between operational semantics state-based definitions of ADT (Abstract Data Types) and programs can be given an event based LTS (Labeled Transition System) semantics. In ICFEM03 we define a generic definition of refinement that is parameterized on the contexts in which they can be placed. By defining the contexts we can obtain standard for handshake processes or ADTs. In FACS05 we use this again to give a model of broadcast processes.

In Constructing Programs or Processes we find that determinism is defined to be conceptually quite different on ADTs defined in the state based world and on handshake processes defined in the event based world. We also come the the conclusion, much to our supprise, that even the simplist branching hand shake process defined in process algebras CSP,CCS,ACP etc. can not actually be accurately implemented.

In FACS 2005 we illustrate a simple "use case" style specification of a handshake processes that can not be satisfied using the atomic actions that appear in the specification. We define a notion of vertical refinement and explore how we might implement a high-level handshake layer on a low-level broadcast layer. The problems we encounter bring us back the exactly the same processes that in Constructing Programs or Processes we concluded we could not implement.

Currently we are interested in Constructible Processes, how to implement them on a broadcast layer and how such a model would work with use case style specifications.

Papers

Published

FM 2009
S. Reeves, D. Streader, LNCS 5850 , A robust semantics hides fewer errors
Refine 2009
S. Reeves, D. Streader, (to appear) ENTCS, Elsevier, Guarded operations, refinement and simulation
Refine 2008
S. Reeves, D. Streader, ENTCS, Volume 214, Elsevier, General Refinement, Part One: interfaces, determinism and special refinement
Refine 2008
S. Reeves, D. Streader,ENTCS, Volume 214, Elsevier, General Refinement, Part Two: flexible refinement
Formal Aspects of Computing 2008
S. Reeves, D. Streader, Data refinement and singleton failures refinement are not equivalent
TTSS 2007
S. Reeves, D. Streader, Generic tools via general refinement ENTCS , TTSS07
SEFM 2007
S. Reeves, D. Streader, Feature Refinement , IEEE Computer Society
ICECCS 2007
Petra Malik, Robi Malik, David Streader, Steve Reeves, Modular Synthesis of Discrete Controllers, ICECCS07
International Journal of Foundations of Computer Science 17(4) 2006
R. Malik, S.Reeves and D.Streade, Conflicts and Fair Testing International Journal of Foundations of Computer Science 17(4)
Journal of Universal Computer Science 11(12) 2005
S.Reeves and D.Streader, Constructing Programs or Processes
FACS 2005
S.Reeves and D.Streader, Stepwise Refinement of Processes , ENTCS Elsevier. Volume 160, 8 August 2006, Pages 275-289
ATVA 2004
R. Malik, S.Reeves and D.Streader, LNCS 3229, Fair Testing Revisited: a Process-Algebraic Characterisation of Conflicts
ICTAC 2004
S.Reeves and D.Streader, p 128-139, LNCS 3407 Atomic Components
ICFEM 2003
S.Reeves and D.Streader, Comparison of data and process refinement, LNCS 2885 Small Revision 2004
ST.EVE 2003
S.Reeves and D.Streader, (State and Events Workshop) Value passing and refinement

Work still in progress

Guarded operations refinement and simulation2009
S.Reeves and D.Streader, Regaining the soundness and joint completeness of forward and backward simulation w.r.t. sF refinement
Constructing Programs or Processes
S.Reeves and D.Streader, Constructing Programs or Processes
CPA
S.Reeves and D.Streader, Causal process Algebra, or always getting the right drink from a coffee machine
Stepwise Refinement
S.Reeves and D.Streader, Stepwise Refinement
Workingpaper 07/2006
S.Reeves and D.Streader, Liberalising Event B (Without changing it)
Workingpaper 08/2006
S.Reeves and D.Streader, LSB - Live and Safe B (Alternative semantics for Event B)
Workingpaper 09/2006
S.Reeves and D.Streader, State- and Event-based refinement
Workingpaper 02/2007
S.Reeves and D.Streader, Flexible Refinement
Workingpaper 02/2009
S.Reeves and D.Streader, Guarded operations, refinement and simulation
Workingpaper 03/2009
S.Reeves and D.Streader, A robust semantics hides fewer errors

Slides
Refine 2005 FACS 2005 ACM05 CStalk ZNZ TTSS07 UTT SIENZ07 Refine08 MetaB08 FM09 BYO-Refinement09
Teaching
2007(B) Comp242 2009(B) Comp104 + Comp204



David Streader 2004-03-12