ProVotE is a two-phase pro ject aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino, which will be held in November 2008. During the first phase of the ProVotE pro ject we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 vot- ers during local elections held in various municipalities of Trentino (Italy). A critical component of jprovote is its core logic, that is re- sponsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its devel- opment and to allow for formal verification of this critical component we developed FSMC+. FSMC+ is a compiler that takes as input a subset of UML statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distin- guishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e- voting machine. Even though FSMC+ has been specifically created to ease the development of jprovote, we believe the approach and the tool we developed to be general enough to be used in other applications.
FSMC+, a tool for the generation of Java code from statecharts
Tiella, Roberto;Villafiorita Monteleone, Adolfo;
2007-01-01
Abstract
ProVotE is a two-phase pro ject aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino, which will be held in November 2008. During the first phase of the ProVotE pro ject we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 vot- ers during local elections held in various municipalities of Trentino (Italy). A critical component of jprovote is its core logic, that is re- sponsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its devel- opment and to allow for formal verification of this critical component we developed FSMC+. FSMC+ is a compiler that takes as input a subset of UML statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distin- guishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e- voting machine. Even though FSMC+ has been specifically created to ease the development of jprovote, we believe the approach and the tool we developed to be general enough to be used in other applications.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
