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