creators_name: Joochim, Tossaporn creators_name: Snook, Colin creators_name: Poppleton, Mike creators_name: Gravell, Andrew type: conference_item datestamp: 2012-07-23 10:20:34 lastmod: 2012-07-23 10:20:34 metadata_visibility: show title: TIMING DIAGRAMS REQUIREMENTS MODELING USING EVENT-B FORMAL METHODS ispublished: pub subjects: deploy_method_other subjects: deploy_method_reqevo full_text_status: none pres_type: paper keywords: Visual and Formal modeling, Timing diagram, Event-B, UML-B note: Event Dates: February 16 ? 18, 2010 abstract: Timing diagrams provide an intuitive graphical specification for time constraints and causal dependencies between a system?s objects. Such a view can provide useful insight during Requirements Engineering (RE). Formal Modeling techniques allow abstract system level models to be explored in revealing detail and provide feedback via verification and validation methods such as proofs of consistency, model checking and animation. Here, we bring these two modelling approaches together. In particular we present techniques to extend a graphical modeling capability for formal modeling into the real-time domain by developing a Timing diagram view for the Event-B formal method and its graphical front-end, UML-B. Translation schemes to Event-B and UML-B are proposed and presented. A case study of a lift system is used to demonstrate the translation in practice. date: 2010-02 date_type: published publisher: ACTA Press event_title: IASTED International Conference on Software Engineering (SE2010) event_type: conference refereed: TRUE official_url: http://eprints.soton.ac.uk/268489/ citation: Joochim, Tossaporn and Snook, Colin and Poppleton, Mike and Gravell, Andrew (2010) TIMING DIAGRAMS REQUIREMENTS MODELING USING EVENT-B FORMAL METHODS. In: IASTED International Conference on Software Engineering (SE2010).