Grant: Discovery Grants Program - Individual
Concordia University
$3,230.00
Practical advances in the formal verification of security and safety critical software
EF 2011-12
Résumé
It is estimated that faulty software costs the world economy 160 billion dollars yearly. Hence, efforts that can be made to help improve software reliability, even in a small way, will be worthwhile. Sir Tony Hoare and other eminent researchers recently determined that the ""time was right"" to revive Robert Floyd's 1967 Verifying Compiler (VC) project. They did so by recasting the project in the form of a Grand Challenge for Computer Science and Software Engineering known as Grand Challenge 6 (GC6), Dependable Systems Evolution. In summary, the GC6 is an international effort with a time scale of 15-20 years whose main deliverables consist of: (i) Unified theory of software analysis and construction; (ii) Verifying Compiler (VC), a tool that can establish the correctness of a program, relative to its specification, before it is run; (iii) Verified Software Repository (VSR) of industrial grade applications and their specifications. The overall research goal behind this proposal is to contribute to the development of theories, languages, tools and methodologies which can help the software industry be more effective at developing quality software. Work towards this goal will be through contributions to the GC6 with a focus on the Java Modeling Language (JML), a Behavioral Interface Specification Language (BISL) for Java because of Java's use in security and safety critical areas such as Web-based Enterprise Applications (WEAs) and embedded devices and controllers (such as smart cards). Specific projects within the scope of this proposal include: (1) compounding the benefits of Runtime Assertion Checking, Extended Static Checking, Full Static Program Verification and Model Checking; (2) unification of JML axiomatizations, mutliprover support, parallel verification; (3) enhancements to the language design and semantic foundation of JML; (4) industrial case studies. The combined advances set forth in the proposal are novel. They will help raise the bar on the size of applications that can be subject to formal verification using JML tools.
Programme
Discovery Grants Program - Individual
Bénéficiaire
Emplacement
Quebec, Canada
Type de bénéficiaire
Academia
Type
Grant
Source
NSERC's Awards Data
Tel que publié
Application id
261573-2008
Name nom
Chalin, Patrice
Department département
Computer Science and Software Engineering
Organization id
70
Institution établissement
Concordia University
Province en
Québec
Province fr
Québec
Country en
CANADA
Country fr
CANADA
Fiscal year exercice financier
2011
Competition year année de concours
2008
Award amount
3230
Program id
RGPIN
Program nane en
Discovery Grants Program - Individual
Program name fr
Programme de subventions à la découverte - individuelles
Group en
Discovery grants programs
Group fr
Programmes de subventions à la découverte
Committee code
330
Committee name en
Computing and Information Sciences - A
Committee name fr
Informatique - A
Area of application code
801
Area of application group en
Information and communication services
Area of application group fr
Services d'information et de télécommunications
Area of application en
Computer software
Area of application fr
Logiciel
Research subject code
2706
Research subject group en
Information technology
Research subject group fr
Technologie de l'information
Research subject en
Software engineering
Research subject fr
Génie logiciel
Partie
4
Nb partie
4
Application title
Practical advances in the formal verification of security and safety critical software
Keyword
NSERC
Application summary
It is estimated that faulty software costs the world economy 160 billion dollars yearly. Hence, efforts that can be made to help improve software reliability, even in a small way, will be worthwhile. Sir Tony Hoare and other eminent researchers recently determined that the ""time was right"" to revive Robert Floyd's 1967 Verifying Compiler (VC) project. They did so by recasting the project in the form of a Grand Challenge for Computer Science and Software Engineering known as Grand Challenge 6 (GC6), Dependable Systems Evolution. In summary, the GC6 is an international effort with a time scale of 15-20 years whose main deliverables consist of: (i) Unified theory of software analysis and construction; (ii) Verifying Compiler (VC), a tool that can establish the correctness of a program, relative to its specification, before it is run; (iii) Verified Software Repository (VSR) of industrial grade applications and their specifications. The overall research goal behind this proposal is to contribute to the development of theories, languages, tools and methodologies which can help the software industry be more effective at developing quality software. Work towards this goal will be through contributions to the GC6 with a focus on the Java Modeling Language (JML), a Behavioral Interface Specification Language (BISL) for Java because of Java's use in security and safety critical areas such as Web-based Enterprise Applications (WEAs) and embedded devices and controllers (such as smart cards). Specific projects within the scope of this proposal include: (1) compounding the benefits of Runtime Assertion Checking, Extended Static Checking, Full Static Program Verification and Model Checking; (2) unification of JML axiomatizations, mutliprover support, parallel verification; (3) enhancements to the language design and semantic foundation of JML; (4) industrial case studies. The combined advances set forth in the proposal are novel. They will help raise the bar on the size of applications that can be subject to formal verification using JML tools.
