Affordable Access

Timing diagrams add Requirements Engineering capability to Event-B Formal Development

Authors
Publication Date

Abstract

Microsoft PowerPoint - March_3_08.ppt Timing diagrams add Requirements Engineering capability to Event-B Formal Development Tossaporn Joochim Supervisor : Dr. Michael R. Poppleton Dependable System and Software Engineering group School of Electronics and Computer Science University of Southampton 2 Outline • Event-B model structure • Timing diagrams � Notations � Case study : The Lift System • Pattern to transform Timing diagrams into an Event-B model � BNF definitions � Translation rules • Conclusions and Future work 3 Event-B • Structure of Event-B MACHINE name SEES context’s name VARIABLES ….. INVARIANT ….. INITIALISATION ….. EVENTS eventname = ...... eventname = ...... END CONTEXT SEES This Presentation 4 Event-B (cont’) • The general form of an event is E = ANY l WHERE G(l,v) THEN S(l,v) END (1) • A short form of an event omitting local variables is E = WHEN G(v) THEN S(v) END (2) 5 Case study : The Lift System Some specifications are described as follows a) The moving lift will be stopped at the requested floor within a time interval of 2 – 5 seconds after floor sensor is set on. b). If the lift becomes stationary, the direction lamp must be deactivated immediately. c). Whenever the lift starts moving up/down, the current floor sensor will be off within a time interval of 2 – 5 seconds after the lift starts moving. ………………. ………………. 6 Parts : BNF Timing Diagrams definitions A Timeline comprises a chain of segments which individual segment represents the object state (Objst) and its position (Index) in the Timeline. Timeline ::= Segment+ Segment ::= Objst Index Index ::= integer 7 Translation rules Rule 4: ������(Class) � SqParam This rule gives the sequence of parameters for an input class. This rule gives the class for an input object. Rule 3: ������(Obj) � Class This rule gives the object for an i

There are no comments yet on this publication. Be the first to share your thoughts.