Altran Praxis English language selection button
Altran Praxis French language selection button
Altran Praxis English language label
Altran Praxis Logo
Altran Praxis Technology image

CbyC

What is Correctness by Construction?

Correctness by Construction was defined in order to capture Praxis’ lessons learnt on eliminating or removing defects from software in the cheapest way possible. Put another way, it captures Praxis’ approach to engineering quality into software in the most cost-effective manner.

Correctness by Construction is an engineering philosophy that combines defect avoidance with rapid defect removal in such a way as to minimise waste and maximise value. The philosophy is based on a set of engineering fundamentals and is underpinned by an integrated set of Altran Praxis methods and supported tools.

Other non-Praxis proprietary methods and tools can be and have been used with Correctness by Construction.

Correctness by Construction has not been designed to meet any one particular regulatory environment but can meet them all.

Why is Correctness by Construction different?

The prime differentiators are as follows.
  • The techniques Praxis uses such as REVEAL®, Formal Computing, INFORMED and SPARK have a high impact, particularly at the front end of the lifecycle.
  • The use of formality and rigour through-out the life-cycle.
  • Strong static verification.
  • Evidence collected ‘as you go’. This aspect is in line with emerging objectives-based safety standards such as Def Stan 00-56 Issue 4.
  • Published productivity, cost and defect-rate metrics.

What is Praxis’ pedigree with Correctness by Construction?

Correctness by Construction has evolved through a series of distinct engineering achievements dating back to the foundation of Praxis.
  • The achievement of BS5750/ISO9001 accreditation (the first UK software company to do so) set out an important process culture for Praxis.
  • The early 1980s saw the company’s first large-scale application of formal methods, with the production of the CDIS Air Traffic Control system. CDIS was the first project for which Praxis offered a warranty and produced a safety case – the system is still in live operation.
  • The SPARK technology arrives at Praxis in 1994 through the acquisition of Program Validation Limited.
  • The production of SHOLIS (Ship Helicopter Landing Information System) was the first Defence Standard 00-55 SIL 4 project and saw the application of Z, Z Proof, and SPARK Proof. No defects were found during customer acceptance and experience from this work was published in IEEE Transactions in Software Engineering.
  • The C130J heavy aircraft project saw the first brown-field application of SPARK and a retrospective application of code proof.
  • The REVEAL® requirements engineering method, based upon the work of Michael Jackson, became codified.
  • The Multos Certification Authority project was the first integrated deployment of Correctness by Construction and saw REVEAL®, Z/CSP, SPARK, Proof and Model Checking deployed, as well as being assured to the highest level of security accreditation.
  • The production of an underwater electronic counter measures SIL 3 software system saw the use of SPARK with static verification in a new domain.
  • A fast-jet test set saw Correctness by Construction techniques cost-effectively used on a SIL 0 system.
  • Tokeneer is a biometric demonstrator that used REVEAL®, Z, SPARK, INFORMED and Proof. Tokeneer was independently verified and is now an open-source non-Praxis data point.
  • The production of a gas turbine engine health monitoring unit saw the application of a partially formal specification, UML™, INFORMED, SPARK and a SPARK-to-C translator.
  • iFACTS remains the largest Correctness by Construction project and has informed Praxis’ view on scale particularly.

How do customers access Correctness by Construction?

Customers can buy Correctness by Construction services in a range of ways.
  • Praxis provides training courses – from a half-day overview of the approach through to week-long courses in underlying methods and techniques.
  • Praxis can deploy on-site teams to work with customers to mentor and support Correctness by Construction developments.
  • Praxis can provide a complete off-load for software development.