Formal object-oriented development of a voting system test oracle

1. Abrial JR (2010) Modeling in Event-B—System and Software Engineering. Cambridge University Press, Cambridge

   MATH  Google Scholar 

2. Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transf 12: 447–466

   Article  Google Scholar 

3. Bouquet F, Dadeau F, Groslambert J (2005) Checking JML specifications with B machines. In: Treharne H, King S, Henson MC, Schneider SA (eds) ZB, Lecture notes in computer science, vol 3455. Springer, Berlin Heidelberg, pp 434–453

   Google Scholar 

4. Cansell D, Gibson JP, Méry D (2007) Refinement: a constructive approach to formal software design for a secure e-voting interface. Electron Notes Theor Comput Sci 183: 39–55

   Article  Google Scholar 

5. Chalin P, Kiniry JR, Leavens GT, Poll E (2005) Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer FS, Bonsangue MM, Graf S, de Roever WP (eds) FMCO, Lecture notes in Computer Science, vol 4111. Springer, Berlin, pp 342–363

   Google Scholar 

6. Chaum D (2004) Secret-ballot receipts: true voter-verifiable elections. In: IEEE security & privacy vol 2, No 1. IEEE, pp 38–47

7. Cheon Y, Leavens GT (2002) A simple and practical approach to unit testing: the JML and JUnit way. In: Proceedings of the 16th European conference on object-oriented programming, ECOOP’02. Springer-Verlag, London, UK, pp 231–255

8. Edmunds A, Butler M (2008) Linking Event-B and concurrent object-oriented programs. Electron Notes Theor Comput Sci 214: 159–182

   Article  Google Scholar 

9. Fontaine C, Galand F (2007) A survey of homomorphic encryption for nonspecialists. EURASIP J Inf Secur 2007: 1–15

   Article  Google Scholar 

10. Gibbs TH, Malloy BA, Power JF (2002) Automated validation of class invariants in C++ applications. In: Proceedings of the 17th IEEE international conference on automated software engineering, ASE’02. IEEE Computer Society, Washington, DC, USA, pp 205–215

11. Gibson JP (1993) Formal object oriented development of software systems using LOTOS. Thesis CSM-114, Stirling University

12. Gibson JP, Lallet E, Raffy JL (2008) Analysis of a distributed e-voting system architecture against quality of service requirements. In: The third international conference on software engineering advances (ICSEA 2008). IEEE Computer Society, pp 58–64

13. Gibson JP, Lallet E, Raffy JL (2009) Feature interactions in a software product line for e-voting. In: Feature Interactions in Software and Communication Systems X. IOS Press, pp 91–106

14. Gibson JP, Lallet E, Raffy JL (2010) Engineering a distributed e-voting system architecture: meeting critical requirements. In: Architecting Critical Systems, First International Symposium, ISARCS 2010, Prague, Czech Republic, June 23–25, 2010, Proceedings, vol 6150. Springer, pp 89–108

15. Hagar J, Bieman JM (1996) Using formal specifications as test oracles for system-critical software. Ada Lett XVI: 55–72

    Article  Google Scholar 

16. Kiniry JR, Morkan AE, Cochran D, Oostdijk M, Hubbers E (2006) Formal techniques in a remote voting system. SIGSOFT Softw Eng Notes 31(6): 1–2

    Article  Google Scholar 

17. Richters M, Gogolla M (2000) Validating UML models and OCL constraints. In: Evans A, Kent S, Selic B (eds) UML Lecture notes in computer science, vol 1939. Springer, Berlin, pp 265–277

    Google Scholar 

18. Said MY, Butler MJ, Snook CF (2009) Language and tool support for class and state machine refinement in UML-B. In: Cavalcanti A, Dams D (eds) FM, Lecture notes in computer science, vol 5850. Springer, Berlin, pp 579–595

    Google Scholar 

Download references