MCLab Group List of Papers
Home
|
Show All
|
Simple Search
|
Advanced Search
Login
Quick Search:
Field:
main fields
author
title
publication
keywords
abstract
contains:
...
1–1 of 1 record found matching your query (
RSS
):
Search & Display Options
Search within Results:
Field:
author
title
year
keywords
abstract
type
publication
abbrev_journal
volume
issue
pages
thesis
publisher
place
editor
series_title
language
area
issn
isbn
notes
call_number
serial
contains:
...
Exclude matches
Display Options:
Field:
all fields
keywords & abstract
additional fields
records per page
Select All
Deselect All
<<
1
>>
List View
|
Citations
|
Details
Record
Links
Author
Pugliese, Rosario; Tronci, Enrico
Title
Automatic Verification of a Hydroelectric Power Plant
Type
Conference Article
Year
1996
Publication
Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3
Abbreviated Journal
Volume
Issue
Pages
425-444
Keywords
Abstract
We analyze the specification of a hydroelectric power plant by ENEL (the Italian Electric Company). Our goal is to show that for the specification of the plant (its control system in particular) some given properties hold. We were provided with an informal specification of the plant. From such informal specification we wrote a formal specification using the CCS/Meije process algebra formalism. We defined properties using μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-calculus formulas into BDDs. In this paper we present the informal specification of the plant, its formal specification, some of the properties we verified and experimental results.
Address
Corporate Author
Thesis
Publisher
Springer
Place of Publication
Oxford, UK
Editor
Gaudel, M.-C.; Woodcock, J.
Language
Summary Language
Original Title
Series Editor
Series Title
Lecture Notes in Computer Science
Abbreviated Series Title
Series Volume
1051
Series Issue
Edition
ISSN
3-540-60973-3
ISBN
Medium
Area
Expedition
Conference
Notes
Approved
yes
Call Number
Sapienza @ mari @ fme96
Serial
53
Permanent link to this record
Select All
Deselect All
<<
1
>>
List View
|
Citations
|
Details
Home
Library Search
|
Show Record
|
Extract Citations
Help