creators_name: Iliasov, Alexei creators_id: "Alexei Iliasov" type: conference_item datestamp: 2011-10-05 12:32:28 lastmod: 2011-10-29 18:22:06 metadata_visibility: show title: Generation of certifiably correct programs from formal models ispublished: pub subjects: Code_generation subjects: Event-Bsemantics subjects: Proof subjects: deploy_method full_text_status: public pres_type: paper abstract: Application of formal notations and verifications techniques 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 certification 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. date: 2011 date_type: published event_title: 1st Int. Workshop on Software Certification. At the 22nd Int. Symposium on Software Reliability Engineering (ISSRE 2011). event_location: Hiroshima, Japan event_dates: November 30, 2011 event_type: workshop refereed: TRUE citation: Iliasov, Alexei (2011) Generation of certifiably correct programs from formal models. In: 1st Int. Workshop on Software Certification. At the 22nd Int. Symposium on Software Reliability Engineering (ISSRE 2011). , November 30, 2011, Hiroshima, Japan. document_url: http://deploy-eprints.ecs.soton.ac.uk/348/1/main_f.pdf