University of Limerick Institutional Repository

Modelling the haemodialysis machine with Circus

DSpace Repository

Show simple item record

dc.contributor.author Gomes, Arthur O
dc.contributor.author Butterfield, Andrew
dc.date.accessioned 2017-01-16T14:43:14Z
dc.date.available 2017-01-16T14:43:14Z
dc.date.issued 2016
dc.identifier.uri http://hdl.handle.net/10344/5458
dc.description peer-reviewed en_US
dc.description.abstract We present a formal model of aspects of the haemodialysis machine case study using the Circus speci cation notation. We focus on building a model in which each of the software requirements (R-1{36) are represented by a Circus action. All of these act in concert with actions that model the collection of sensor data and the progress through the various therapy phases and activities. We then present how we model check the system using FDR. 1 en_US
dc.language.iso eng en_US
dc.publisher Springer en_US
dc.relation.ispartofseries ABZ 2016 Proceedings of the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z: Lecture Notes in Computer Science (LNCS);9675, pp. 409-424
dc.relation.uri http://dx.doi.org/10.1007/978-3-319-33600-8_34
dc.rights The original publication is available at www.springerlink.com en_US
dc.subject haemodialysis machine en_US
dc.subject software engineering en_US
dc.title Modelling the haemodialysis machine with Circus en_US
dc.type info:eu-repo/semantics/conferenceObject en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.identifier.doi 10.1007/978-3-319-33600-8_34
dc.contributor.sponsor SFI en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


Browse

My Account

Statistics