---
abstract: "This paper proposes a method for deriving formal specifications of systems. To accomplish this task we\r\npass through a non trivial number of steps, concepts and\r\ntools where the first one, the most important, is the concept of method itself, since we realized that computer science has a proliferation of languages but very few methods. We also propose the idea of Layered Fault Tolerant Specification (LFTS) to make the method extensible to Dependable Systems. The principle is layering the specification, for the sake of clarity, in (at least) two different levels, the first one for the normal behavior and the others (if more than one) for the abnormal. The abnormal behavior is described in terms of an Error Injector (EI) which represents a model of the erroneous interference coming from the environment. This structure has been inspired by the notion of idealized fault tolerant component but the combination of LFTS and EI using rely guarantee thinking to describe interference can be\r\nconsidered one of the main contributions of this work. The\r\nprogress toward this method and the way to layer specifications.\r\nhas been made experimenting on the Transportation\r\nand the Automotive Case Studies of the DEPLOY project."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - manuel.mazzara@newcastle.ac.uk
creators_name:
  - family: Mazzara
    given: Manuel
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: ~
datestamp: 2009-10-01 15:51:18
department: ~
dir: disk0/00/00/01/57
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 157
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/157/1/RigorousDevelopment_1.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: 0
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: 2010-04-19 15:05:58
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: ~
producers_id: []
producers_name: []
projects: []
publication: EWDC 2009
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 22
series: ~
skill_areas: []
source: ~
status_changed: 2009-10-01 15:51:18
subjects:
  - deploy_method_other
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'Deriving Specifications of Dependable Systems: toward a Method'
type: article
userid: 217
volume: ~