Mathematical proof techniques, automated requirements tracing are trends in software verification tools

BY John Keller

Complex application software increasingly is finding its way into mission- and life-critical applications, like medical equipment, surveillance and reconnaissance systems, and even high-end passenger cars. Despite the importance of this software, however, much of today’s sophisticated code is developed in somewhat of a haphazard manner with little foolproof debugging going on, and even less code verification based on formal methods.

“The modern car has more lines of code than a typical commercial jetliner,” says Robert Dewar, president and chief executive officer of AdaCore Technologies Inc. in New York. “Medical instrumentation has critical software that also is written in a haphazard way,” he says.

Software in these kinds of mission- and life-critical systems could learn a thing or two from aerospace and defense technology, such as avionics and military systems in which formal certification is mandatory, and where the use of software verification tools are seeing increasing use not only to find software bugs, but also to exercise the software automatically in a wide variety of scenarios to ensure the code will work every time.

Approaches to software verifi- cation tools are widely varied, but tend to segment into static tools, which work with the source code itself, and dynamic test tools, which execute the code with test cases to verify that the software works correctly. New kinds of dynamic software code verification tools seek to automate the process of following software verification requirements.

In addition, software engineers are working on developing formal, mathematical proof techniques to ensure code quality. Among the companies invested in formal mathematical proof techniques for software code verification is The MathWorks in Natick, Mass.

“There is a new class of verification tools that actually analyzes the code to check to make sure there won’t be a certain class of runtime errors,” says Jon Friedman, aerospace and defense industry marketing manager at The MathWorks. “These check to make sure that the engineer hasn’t left openings for those kinds of problems.”

Formal, mathematically provable methods are absolutely essential for removing all doubt that software will work when called on, says Jay Abraham, product marketing manager at The MathWorks. “You cannot do exhaustive software testing without formal methods,” Abraham says. “Formal mathematics can boil down these complicated problems into smaller problems that you can prove.”

AdaCore’s Dewar says use of mathematical proof techniques is a major trend in software verification tools today. He says this technology should be mature within the next five years. “It is being used today, but it is not yet standard industry practice,” Dewar says.

Today’s high-performance and relatively inexpensive computing is helping software engineers implement formal methods in software code verification. In years past, the kind of computing necessary to run formal methods was unavailable to most engineers.

Following a set process for soft- ware code verification is not new, but in the recent past has been a laborious process. Today, software engineers are trying to automate that process of tracing requirements all the way down to testing on a target, says Chris Murray, vice president of business development at LDRA Ltd. U.S. office in San Bruno, Calif.

“It is most important to be able to find out which software artifact is connected upstream or downstream to another artifact,” Murray says. “You need to do that quickly and efficiently. LDRA does that with a tool called Object Box, which is a component of the LDRA Tool Suite that includes static and dynamic software testing and requirements traceability.”

More Military & Aerospace Electronics Current Issue Articles
More Military & Aerospace Electronics Archives Issue Articles


Easily post a comment below using your Linkedin, Twitter, Google or Facebook account.


Military & Aerospace Photos

Most Popular Articles

Related Products

SBC-K7 Embedded PC for Instrumentation and Control

The SBC-K7 is an ideal platform for embedded instrumentation that combines an Atom PC running Win...

Rugged Mobile Communications Server

Advanced communications server designed to be deployed in environments where it needs to meet cer...

RR2P Removable Canister RAID System

Transportable data storage for mobile field use aboard planes, ships and ground transport. 2U, du...

Sensors Unlimited GA1280JSX High Resolution, Mil-Rugged, Extended High Sensitivity InGaAs SWIR Camera

Manufactures a high resolution, mil-rugged, extended high-sensitivity 0.9 Mpixel InGaAs SWIR came...

M1U20xx 1U Military-Grade Computer System

The M1U20xx Military-Grade Rack Mount System is a reliable high-performance mil-spec 1U solution ...

TFX-19 Trifold Rackmount LCD

The TFX1-19 is a rugged military grade high performance 2U rackmount LCD panel display offering t...

P317xx Portable Computer System w/ Three 17" LCDs

The P317xx portable " lunchbox" system is unique in offering three 17" 1280x1024 resolution LCD d...

CCXR-17 Slideways Side Access Rackmount LCD Keyboard

The CCXR-17 is a unique Side Access space-efficient military-grade high-performance 1U rackmount ...

M4U20xx 4U Rackmount Military-Grade Computer

A 4U rugged military-grade computer offering the latest long-availability high-performance mother...

Large Fiber Collimators

Diffraction Limited Large Fiber Collimators are designed for long distance beam propagation with ...

Related Companies

Innovative Integration

  Since 1988, Innovative Integration has grown to become one of the world's leading suppliers of DSP and data ac...

Elma Electronic Inc

Who we are...   About Elma Electronic Systems   The Systems division of Elma Electronic Inc. supplies the

Winchester Systems Inc

At its founding in 1981, Winchester Systems introduced its first 5 MB disk system for Intel development system users....

Extreme Engineering Solutions Inc (X-ES)

 Extreme Engineering Solutions, Inc. (X-ES) is a leader in the design, manufacture, and support of standard and ...

American Infrared Solutions (AIRS)

American Infrared Solutions

GE Intelligent Platforms

GE Intelligent Platforms is a leading global provider of embedded computing systems and modules for a wide range of a...

Raycom Electronics

Raycom Electronics, Inc., a subsidiary of Electro Technik Industries (ETI), was incorporated in 1965.  The compa...

Trenton Systems Inc

Designs and manufactures rugged rackmount computers and MIL-STD-810 systems using both standard COTS as well as custo...

Sensors Unlimited - UTC Aerospace Systems

Manufactures near-IR (NIR) and shortwave IR (SWIR) cameras (available fully packaged or as OEM imaging modules), line...
Wire News provided by   

social activity

Webcasts

Meeting the Gen3 backplane challenge with OpenVPX and COTS

Tight Pentagon budgets mean military systems must stay in the field for longer than ever before. This doesn't mean obsolete technology, however. Today's military electronics are being upgraded constantly, an...
Sponsored by:

Digital signal processing for signals intelligence and electronic warfare

Military & Aerospace Electronics presents an expert Webcast on the design considerations for blending general-purposes processors (GPUs), general-purpose graphics processors (GPGPUs), field-programmable ...
Sponsored by:

Advantages of Intel Architecture Products and Wind River Solutions in Military & Aerospace Applications

This webinar explains the individual advantages of the Intel Architecture hardware, available for long-life supply, and the WRS software portfolio.  There are extraordinary advantages of combining such ...
Sponsored by:

All Access Sponsors

View the 2014 Buyer's Guide Now!


Mil & Aero Magazine

October 2014
Volume 25, Issue 10
file

Download Our Apps



iPhone

iPad

Android

Follow Us On...



Newsletters

Military & Aerospace Electronics

Weekly newsletter covering technical content, breaking news and product information
SUBSCRIBE

Defense Executive

Monthly newsletter covering business news and strategic insights for executive managers
SUBSCRIBE

Electronic Warfare

Quarterly newsletter covering technologies and applications in electronic warfare, cyber warfare, optical warfare, and spectrum warfare.
SUBSCRIBE

Embedded Computing Report

Monthly newsletter covering news on embedded computing in aerospace, defense and industrial-rugged applications
SUBSCRIBE

Unmanned Vehicles

Monthly newsletter covering news updates for designers of unmanned vehicles
SUBSCRIBE