---
abstract: "Abstract—A large number of dependable embedded systems\r\nhave stringent real-time requirements imposed on them. Analysis of their real-time behaviour is usually conducted at the implementation level. However, it is desirable to obtain an evaluation of real-time properties early at the development cycle, i.e., at the modelling stage. In this paper we present an approach to augmenting Event-B modelling with verification of real-time properties in Uppaal. We show how to extract a process-based view from an Event-B model that together with introducing time constraints allows us to obtain a timed automata model – an input model of Uppaal. We illustrate the approach by development and verification of the data processing software of the BepiColombo Mission."
accompaniment: []
book_title: 'Proc. of Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches held in conjunction with ICSE 2012. 2 June 2012, Zurich, Switzerland.'
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - '"Alexei Iliasov" <Alexei.Iliasov@newcastle.ac.uk>'
  - Linas.Laibinis@abo.fi
  - Elena.Troubitsyna@abo.fi
  - alexander.romanovsky@ncl.ac.uk
  - ~
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
  - family: Laibinis
    given: Linas
    honourific: ''
    lineage: ''
  - family: Troubitsyna
    given: Elena
    honourific: ''
    lineage: ''
  - family: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
  - family: Latvala
    given: Timo
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: published
datestamp: 2012-03-30 14:10:28
department: ~
dir: disk0/00/00/03/85
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 385
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/385/1/main2.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: ~
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2012-03-30 14:10:28
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: 7
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ACM
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 5
series: ~
skill_areas: []
source: ~
status_changed: 2012-03-30 14:10:28
subjects:
  - Event-Bsemantics
  - Refinement
  - deploy_tooldev_modelc
  - deploy_tooldev_rodinplugins
  - rt_modelling
succeeds: 384
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Augmenting Event-B Modelling with Real-Time Verification
type: book_section
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>