Software Tools

Every business is experiencing an increasing reliance on distributed processing systems and software. Whether as part of a product or the support of a service, the reliability of these systems is often critical to business success and continuity. Failure of these systems can result in loss of business reputation, high recall or support costs and in the worst cases, loss of life.

Conventional testing is becoming increasingly expensive as the complexity of the software system grows, but validation and verification is required to reduce the risk of system failure. Coupled with the increasing business risk that systems and software create, is the government authorities' wish to apply global measures to ensure safety and correct operation. As users and consumers, we should feel comforted that Aerospace applies certification requirements such as DO-178B, Automotive are instigating ISO 26262 and Rail EN 50218&9 to force these sectors into a compliance regime that guarantees reasonable safety.

It is well documented that for systems and software development, the most efficient path in terms of time and cost is to identify errors as early as possible in the development process so avoiding rework. The key to affordable error free systems is the use of the emerging technique of "Formal Methods" in the automation of systems requirements capture and the automation of ensuring software code implements the required design, as well as providing the evidence to meet certification requirements.

Formal Methods is a mathematical process from which D-RisQ has produced two systems and software development tools.

  • Modelworks® ensuring the systems requirement capture and
  • CLawZ® ensuring the code implements the design.

The automation of these processes can reduce the test and verification costs by over 50% over normal manual test methods.

CLawZ®

CLawZ® is a toolset that independently verifies through proof that code generated from a Simulink model is a refinement, i.e. correct. The toolset consists of a Z producer, a Refinement Script Generator, a compliance tool for the target source code language, and a theorem prover.

The Z producer automatically generates a specification statement where the pre-condition and post condition are represented in the Z language. The Refinement Script Generator generates a refinement conjecture, i.e. it constructs a top down refinement as though the code had been incrementally developed from the specification. The compliance tool processes the refinement conjecture and generates verification conditions in the Z language. If the verification conditions are proven then the refinement conjecture holds and the code is a correct implementation of the Simulink model.
The verification conditions are automatically proven, or simplified for human review. The automated reasoning is carried out by a set of proof tactics called Supertac which direct the theorem prover, called ProofPower on how to simplify and discharge the verification conditions. The CLawZ® toolset was developed and refined over a period of 10 years in order to independently verify the flight and engine control system software as well as the autopilot and auto-throttle software for Eurofighter Typhoon. The semantic validity of the Z producer has been established over that period as well as the effectiveness of the automated proof capability of Supertac.

To investigate using this new technology to reduce risk, lower development costs, reduce support and warranty costs and reduce time to market, please click here for a D-RisQ consultant to provide more detail or click here to refer us to your technical expert with responsibility for systems and software Development.


Enter your email address below to obtain a copy of our CLawZ® overview document by return.



CAPTCHA code image
Speak the codeChange the code
 
Request your document           

Modelworks®

Modelworks® is a tool that compiles distributed state machines into a machine readable dialect of the process algebra of Communicating Sequential Processes, CSPm. Each state machine takes the form of a precondition that enables an action. The state machines communicate with each other over various pre-defined media that have specified properties such as: being asynchronous or synchronous; being point-to-point or broadcast; being fallible through message loss, or re-ordering, or late delivery etc.

Failures can be injected into the systems represented in Modelworks® to model failures that can arise from faulty components such as when software does not behave as intended. The eventual representation in CSPm has been carefully optimised to be efficient with respect to the process of refinement model checking. Model checking is simply the exploration of a finite set of states1 to determine whether specified properties hold.

Most model checkers are symbolic based on (Ordered) Binary Decision Diagrams (BDD) that can represent large sets of states by, hopefully relatively small logical formulae. The model checking employed by Modelworks® uses explicit-state exploration. This has the advantage that it is not necessary to calculate the entire transition relation in advance; it can be evolved on-the-fly.

Recent advances in the model checker for Modelworks® means that it can exploit parallel cores on modern laptops. This has led to significant performance increases that compare favourably with existing model checkers throughout the world. The performance increase means that system components can be checked at a level of granularity that does not require human intervention to exploit a divide and conquer strategy. Human generated models already break down into subsystems and components; it is just a matter of being able to automatically check these parts and then compose the parts together to produce an overall check of the system.

Modelworks® supports compositional reasoning because it supports refinement checking (where a model of a system satisfies a specification of that system) and because CSPm is inherently compositional. Indeed this approach has been used as part of an induction argument to prove properties of infinite systems. Modelworks® has a front end that semantically translates a Simulink Stateflow model into Modelworks® for analysis. Front ends for SysML and UML will be developed in the near future.


1Note that although the system may have a finite set of states, the system can still exhibit infinite repeated behaviours.

 

Enter your email address below to obtain a copy of our Modelworks® overview document by return.



CAPTCHA code image
Speak the codeChange the code
 
Request your Document           

D-RisQ Limited

Malvern Hills Science Park

Geraldine Road
Malvern
Worcestershire
United Kingdom
WR14 3SZ
+44(0)1684 252452
info@drisq.com

Company Number: 7754903

What we do?

With a wide experience in analysis of complex systems and software across many sectors ranging from embedded systems to IT, safety and security critical systems, automotive, aerospace, robotics and many others, D-RisQ has developed huge experience from which to build automated formal analysis tools.

Learn more