Formal specification and analysis of Accelerated Heartbeat Protocols
| dc.contributor.author | Atif, Muhammad | |
| dc.contributor.author | Mousavi, Mohammad Reza | |
| dc.coverage.spatial | Ottawa Canada | |
| dc.date.accessioned | 2015-12-13T22:23:13Z | |
| dc.date.created | July 12-14 2010 | |
| dc.date.issued | 2010 | |
| dc.date.updated | 2016-02-24T10:04:47Z | |
| dc.description.abstract | We present a formal analysis of all different variations of accelerated heartbeat protocols presented in [M.G. Gouda and T.M. McGuire, Accelerated Heartbeat Protocols, Proc. of ICDCS'98]. We formalize the specification of the protocols both in a process-algebraic and in an automata-theoretic formalism. Then, we formulate some natural functional requirements on the above-mentioned protocols and formalize these requirements. Using model-checking techniques, we verify these requirement on each and every version. We report counter-examples witnessing that the formulated requirements are not satisfied. We propose solutions for different versions of the protocol and model check the fixed versions; the model checking results indicate that the fixed versions indeed satisfy the requirements. | |
| dc.identifier.isbn | 9781617387029 | |
| dc.identifier.uri | http://hdl.handle.net/1885/72665 | |
| dc.publisher | Conference Organising Committee | |
| dc.relation.ispartofseries | Summer Computer Simulation Conference, SCSC 2010, Part of the 2010 Summer Simulation Multiconference, SummerSim 2010 | |
| dc.source | Summer Computer Simulation Conference, SCSC 2010 - Proceedings of the 2010 Summer Simulation Multiconference, SummerSim 2010 | |
| dc.subject | Keywords: Formal analysis; Formal specification and analysis; Functional requirement; Model check; Model-checking techniques; Process algebras; Automata theory; Computer simulation; Model checking; Algebra Formal Analysis; Heartbeat protocols; Model checking; Process algebra; Requirement verification | |
| dc.title | Formal specification and analysis of Accelerated Heartbeat Protocols | |
| dc.type | Conference paper | |
| local.bibliographicCitation.lastpage | 412 | |
| local.bibliographicCitation.startpage | 403 | |
| local.contributor.affiliation | Atif, Muhammad, College of Engineering and Computer Science, ANU | |
| local.contributor.affiliation | Mousavi, Mohammad Reza, Eindhoven University of Technology | |
| local.contributor.authoruid | Atif, Muhammad, u4324099 | |
| local.description.embargo | 2037-12-31 | |
| local.description.notes | Imported from ARIES | |
| local.description.refereed | Yes | |
| local.identifier.absfor | 080100 - ARTIFICIAL INTELLIGENCE AND IMAGE PROCESSING | |
| local.identifier.ariespublication | U3488905xPUB3367 | |
| local.identifier.scopusID | 2-s2.0-84871372932 | |
| local.type.status | Published Version |
Downloads
Original bundle
1 - 1 of 1
Loading...
- Name:
- 01_Atif_Formal_specification_and_2010.pdf
- Size:
- 255.52 KB
- Format:
- Adobe Portable Document Format