Definition – What is Formal Computing?
Formal Computing is the collective term for languages, tools and disciplines that are unambiguous, underpinned by mathematics, and amenable to sound analysis.
Allows early detection of system inconsistency and ambiguity, hence reducing cost of problem resolution (see www.sei.cmu.edu for data on this aspect)
Prevents some class of defect entirely and thus reducing verification costs.
- Allows a rigorous formal statement on the coverage of requirements in the delivered system thus increasing the level of assurance.
Allows the precise documentation of domain assumptions. This is crucial in the development of safety- and security-critical systems and also where systems might be subject to future re-use or evolution. The benefit this provides is of reducing the cost and increasing the quality of subsequent changes.
Where to deploy formal computing
All aspects of system development are amenable to some level of Formal Computing. Ideally, we formalise as early as possible to maximise the benefit achievable.
Functional specification – languages such as Z, B, Mathematica, CSP, and tools such as SCADE provide a mechanism for mathematically modelling the specification of a system. Key properties of such specifications can be proven using techniques such as theorem proving and model-checking. This can be particularly useful for demonstrating safety or security features.
- Formal implementation – languages such as SPARK and RavenSPARK and tools such as the SPARK Examiner and Proof Tools can guarantee that required system properties are maintained through to final implementation. Concurrency profiles (for example Ravenscar) enable analysis of timing behaviour, scheduling, and the absence of deadlock. Quality of software is improved and cost of verification reduced.
Formal test case generation – from formal specifications, we can apply techniques such as equivalence class analysis to derive test cases that trace to requirements and meet objectives for structural coverage. Cost of verification and in particular regression testing is reduced.
How we can Deliver Formal Computing
Intelligent Systems / Altran has a long and distinguished history of being at the forefront of deploying industrial formal computing. We have repeatedly broken new ground, as attested to by our impressive track record of project delivery, conference presentations, and journal papers. Keynote projects include CDIS (1990), SHOLIS (1996), the MULTOS CA (2000), Tokeneer (2003) and iFACTS (Current).
We can offer:
Consultancy on the adoption of formal computing and appropriate languages and tools.
Training and mentoring as part of a formal capability enhancement programme.
Full end-to-end delivery of formal system- and software-engineering projects, or high-assurance components within them.
Advice on how formal computing can meet or exceed contemporary standards such as DO-178B, Def Stan 00-56 (including issue 4), Common Criteria at EAL5 and above, IEC 61508 and its derivatives including the forthcoming DO-178C. SPARK language, SPARK Pro toolset, and associated training.
In addition to the industrial-strength languages and tools available today, Intelligent Systems / Altran maintains an R&D capability, both internally and through partnerships with emerging companies and universities. These include:
Alloy from MIT – a functional specification and modelling notation supported by theorem-proving and SAT-solving tools.
Perfect Developer from Escher Technologies – a formal specification, refinement and code-generation tool.
Model-based design notations and tools, particularly those able to generate SPARK such as:
- ADI’s Beacon
- Esterel’s SCADE Suite
- GeneAuto project for Simulink
- Kennedy-Carter’s iUML UML tool
- ARTiSAN’s Real-Time Studio
- IBM’s Rhapsody-in-Ada
SMT-based theorem proving, where the proofs arising from the Tokeneer project have been used as a competitive case-study for decision procedures at the annual CAV conference.
Reprints of this paper are also available from Intelligent Systems / Altran.
The MULTOS certificate authority.
To specify, build and deliver the certificate authority for the MULTOS smartcard operating system, aiming to meet the requirements of ITSEC E6 (now equivalent to Common Criteria EAL7) as far as possible.
REVEAL™ process for requirements engineering, with formalisation of functional behaviour and security properties in Z. Modelling of the concurrent aspects of the architecture in CSP and model-checking for critical properties using the FDR toolset. Security-enforcing functions implemented in SPARK with flow-analysis and proof of absence of type errors and buffer overflows. Test cases were formally derived from the functional specification with subsequent structural coverage analysis.
100,000 logical lines of code delivered. Four defects reported one year after delivery – a defect rate of 0.04 per thousand lines of code. Results validated and consequently accepted for publication in the prestigious IEEE Software Journal.