A case study in requirement analysis of control systems using UML and B

Colin Snook, Leonidas Tsiopoulos, Marina Walden

Tutkimustuotos: Kirja/lehti/raporttiTutkimusraporttiAmmatillinen

1 Lataukset (Pure)

Abstrakti

When developing critical systems that should be highly dependable we need to ensure that these systems satisfy functional as well as safety requirements. This can be achieved by developing the system with a formal method in a stepwise manner and proving the correctness of each step. For industrial strength systems, though, we need a graphical interface to the formal method. In this paper we develop part of a microplate liquid handling workstation, where we express the informal requirements and the refinements in UML. We translate the UML diagrams to B-action systems with the tool U2B. In the B-action system formalism we then prove the correctness of the development using the provers of the tool Atelier B.
AlkuperäiskieliEnglanti
KustantajaTurku Center for Computer Science (TUCS)
ISBN (painettu)952-12-1174-1
TilaJulkaistu - 2003
OKM-julkaisutyyppiD4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset

Julkaisusarja

NimiTUCS Technical Reports
Vuosikerta533

Sormenjälki

Sukella tutkimusaiheisiin 'A case study in requirement analysis of control systems using UML and B'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Viittausmuodot