---
abstract: "Application of formal notations and verifications\r\ntechniques helps to deliver systems that are free from engineering defects. A code generator is an essential tool for formal development of real-world systems; it transforms models into runnable software quickly, consistently and reproducibly. Commonly, a code generator is a program constructed informally and producing an output that is not formally traced to an input. Industrial standards to the development of safety-critical systems, such as IEC 61508, require a justification for any tool used in a development: extensive prior experience or a formal certification. An extensive experience is often not an option as there are very few sufficiently mature modelling toolsets. The\r\ncertification of a code generator is a major effort increasing costs and development time. We propose an approach where a modeller places no trust whatsoever in the code generation stage but rather obtains software that is certifiable without any further effort. The essence of the approach is in the transformation of a formal model into runnable software that is demonstratively correct in respect to a given set of verification criteria, coming from a requirements document. A Hoare logic is used to embedded correctness criteria into the resultant program; the approach supports design-by-contract annotations to allow developer to mix formal and informal parts with a fair degree of rigour."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - '"Alexei Iliasov" <Alexei.Iliasov@newcastle.ac.uk>'
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
data_type: ~
date: 2011
date_type: published
datestamp: 2011-10-05 12:32:28
department: ~
dir: disk0/00/00/03/48
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 348
event_dates: 'November 30, 2011'
event_location: 'Hiroshima, Japan'
event_title: '1st Int. Workshop on Software Certification. At the 22nd  Int. Symposium on Software Reliability Engineering (ISSRE 2011). '
event_type: workshop
exhibitors_id: []
exhibitors_name: []
fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/348/1/main_f.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: 2011-10-29 18:22:06
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 13
series: ~
skill_areas: []
source: ~
status_changed: 2011-10-29 18:22:06
subjects:
  - Code_generation
  - Event-Bsemantics
  - Proof
  - deploy_method
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Generation of certifiably correct programs from formal models
type: conference_item
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>