Development of a Generic Voter under FoCal

Safety and security are claimed major concerns by the formal FoCaL development environment. In [7] we introduced a safety development cycle customised to FoCaL. In this paper, we examine how to specify and implement a concrete example following this cycle. We show that indeed it is feasible and we present how FoCaL features fit with software best practises like modularity, reuse, fault confinement and maintenance. Key words: formal methods, development cycle, voter, FoCaL

• Type: Conference
• Year: 2009
• Where: TAP
• Authors: Philippe Ayrault, Thérèse Hardin, François Pessaux
• Keywords: Development Cycle, Formal Focal Development, Hardware, Safety Development Cycle, TAP 2009