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


Get All the Military Aerospace Electronics News Delivered to Your Inbox or Your Mailbox

Subscribe to Military Aerospace Electronics Magazine or email newsletter today at no cost and receive the latest information on:


  • C4ISR
  • Cyber Security
  • Embedded Computing
  • Unmanned Vehicles


Get All the Military Aerospace Electronics News Delivered to Your Inbox or Your Mailbox

Subscribe to Military Aerospace Electronics Magazine or email newsletter today at no cost and receive the latest information on:


  • C4ISR
  • Cyber Security
  • Embedded Computing
  • Unmanned Vehicles

Military & Aerospace Photos

Most Popular Articles

Related Products

XCalibur4501 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction-Cooled 6U CompactPCI Module

The XCalibur4501 is a high-performance 6U CompactPCI single board computer that is ideal for rugg...

XPedite7501 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled XMC Module

The XPedite7501 is a high-performance, low-power, XMC module based on the 5th generation Intel® C...

XCalibur4540 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 6U VPX Module

The XCalibur4540 is a high-performance, 6U OpenVPX™, multiprocessing, single board computer that ...

XPedite7530 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 3U CompactPCI Module

The XPedite7530 is a high-performance 3U CompactPCI single board computer that is ideal for rugge...

XPedite7570 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 3U VPX-REDI Module

The XPedite7570 is a high-performance, 3U VPX-REDI, single board computer based on the 5th genera...

XPedite7572 | 5th Gen Intel® Core™ i7 Broadwell-H Based Conduction- or Air-Cooled 3U VPX-REDI Module with SecureCOTS™

The XPedite7572 is a secure and high-performance, 3U VPX-REDI, single board computer based on the...

XCalibur4500 | 5th Generation Intel® Core™ i7 Broadwell-H Processor-Based Conduction- or Air-Cooled 6U CompactPCI Module

The XCalibur4500 is a high-performance 6U CompactPCI single board computer that is ideal for rugg...

Medusa VPX3424

The AcQ Inducom “Medusa”VPX3424 is a 3U OpenVPX™ Single Board Computer (SBC) featuring the T4240 ...

XPand6200 Series | Small Form Factor (SFF) Sub-½ ATR Rugged COTS System utilizing 3U VPX, XMC, and PMC Modules

The XPand6200 Series is a true Commercial-Off-The-Shelf (COTS) Rugged system, supporting many 3U ...

XPedite2470 | 3U VPX Xilinx Virtex-7 FPGA Module with FMC Site and Freescale P1010 Processor

The XPedite2470 is a high-performance, reconfigurable, conduction- or air-cooled, 3U VPX, FPGA pr...

Related Companies

AcQ Inducom

Develops and produces non-certified and certified high-tech modular hardware- and software solutions for on-board and...

United Electronic Industries Inc

UEI is a leader in the PC/Ethernet data acquisition and control, Data Logger/Recorder and Programmable Automation Con...

Advanced Conversion Technology Inc

ACT designs and manufactures, since 1981, an extensive range of AC-DC and DC-DC power supplies (switching, linear, ra...

JuiceBox Energy Inc

JuiceBox Energy develops, engineers and manufactures advanced energy storage systems for residential, government and ...

Electronic Development Labs Inc (EDL)

Since 1943, EDL has strived to provide quality products, outstanding customer service, and superior technical support...

PTC

PTC (Nasdaq: PTC) delivers technology solutions that transform the way companies create, operate and service their pr...

Powell Electronics

An authorized electronic component distributor and experts of military connectors, switches, sensors and relays. Trac...

Eureka Dry Tech

High reliability electronic components utilized in aerospace and defense, requires strict moisture controlled storage...

Germane Systems

Germane Systems designs and manufactures COTS-based rugged high performance computers, servers, and storage systems f...

Sensoray Co Inc

Specializing in the development of custom OEM embedded electronics for industrial, aerospace, defense, medical and se...
Wire News provided by   

Press Releases

Model INCX-4001

The INCX-4001 consists of a high quality audio transceiver specifically designed to implement a complete fiber optic intercom.

Model PS-1210

The PS-1210 is a 1A, 12VDC stand-alone or rack mountable non-switcher (no RF noise) power supply.

Model OS-3121

Optical switches are utilized to disconnect, bypass and reroute fiber optic communications. All of these optical switches are purely optical path, there is no optical to e...

Webcasts

New Design Tools That Help You Develop Radar That Sees the Un-seeable and Detects the Undetectable

Xilinx EW/ISR System Architect, Luke Miller, has new tricks and he’s going to tell you all about them in a new Xilinx Webinar—for free. His Webinar will cover new ways to implement Radar functions including ...
Sponsored by:

Latest from the Paris Air Show

All Access Sponsors


Mil & Aero Magazine

June 2015
Volume 26, Issue 6
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

Cyber Security

Monthly newsletter covering cyber warfare, cyber security, information warfare, and information security technologies, products, contracts, and procurement opportunities
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