ORCID Profile
0000-0001-8365-6993
Current Organisation
University of Surrey
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
Publisher: Springer Berlin Heidelberg
Date: 2010
Publisher: IEEE
Date: 08-2011
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 2020
Publisher: IEEE
Date: 07-2014
DOI: 10.1109/CSF.2014.20
Publisher: Springer Berlin Heidelberg
Date: 2012
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 2019
Publisher: Association for Computing Machinery (ACM)
Date: 11-2016
DOI: 10.1007/S00165-016-0376-0
Abstract: In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.
Publisher: Association for Computing Machinery (ACM)
Date: 09-06-2015
DOI: 10.1145/2746338
Abstract: The Prêt à Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this article, we present our development of the Prêt à Voter design to a practical implementation used in a real state election in November 2014, called vVote. As well as solving practical engineering challenges, we have also had to tailor the system to the idiosyncrasies of elections in the Australian state of Victoria and the requirements of the Victorian Electoral Commission. This article includes general background, user experience, and details of the cryptographic protocols and human processes. We explain the problems, present solutions, then analyze their security properties and explain how they tie in to other design decisions.
Publisher: Springer Berlin Heidelberg
Date: 2013
Location: United Kingdom of Great Britain and Northern Ireland
Location: United Kingdom of Great Britain and Northern Ireland
No related grants have been discovered for Steve Schneider.