TrustInSoft Updates Analyzer Tool, Streamlining Software Verification

Last week at Embedded World North Ameriica, TrustInSoft introduced significant updates to its TrustInSoft Analyzer, a tool that leverages formal methods to enhance software verification processes.

These updates respond to the complexity of modern software systems that have outgrown traditional testing methods, often failing to identify all potential vulnerabilities. With rising regulatory demands and growing concerns over safety, many organizations are now turning to advanced verification methods that can guarantee software accuracy and compliance with stringent standards. 

At the show, All About Circuits interviewed TrustInSoft CEO Caroline Guillaume to hear more about the updates firsthand.

TrustInSoft CEO Caroline Guillaume (left) with All About Circuits' editor-in-chief Jeff Child at the 2024 Embedded World North America in Austin, Texas. 

TrustInSoft Rolls Out TISA Updates

TrustInSoft has introduced significant verification updates to its TISA software, including enhanced user experience, greater precision, and improved compliance with industry standards. 

A major upgrade to the tool is the revamped graphical user interface (GUI), which replaces the previously command-line-based project manager. The interface provides centralized access to project settings, analysis configurations, and results, streamlining team collaboration and minimizing setup errors. TrustInSoft designed the new GUI to simplify project management, enable quicker setups, and unlock the ability to track multiple software verification projects simultaneously.

“The new interface features are designed to enable a software developer to set up their project in an easy way when they set up a new analysis with our tool on a new software module,” says Guillaume, “Now can they set it up easily and fast through an intuitive user interface.”

Root Cause Investigator

Another notable addition is the TrustInSoft Root Cause Investigator, which pinpoints problems by issuing alarms and their root causes. Teams can then fine-tune analysis settings directly from the interface.

“The tool is extremely good at understanding the code in-depth,” says Guillaume. “It can actually pinpoint very precisely to the root cause. Users can actually get alarms on where bugs are triggered, but they can also find exactly where the issue is coming from. This is done through the other interface we've been put in place, which is called the Root Cause Investigator.”

The release also introduces automated driver generation based on function selection. This provides comprehensive code coverage with minimal manual configuration. The new Assisted Analysis Setup feature aids the workflow by providing step-by-step guidance that reduces the likelihood of configuration errors and offers dynamic parameter adjustments tailored to project specifics.

“With our assisted driver generator, you pinpoint the functions or the points of the code where you want tests to be written, and the tool generates them for you,”  says Guillaume.“Then you need to fine-tune the test with questions like ‘Should I test for every possible entry? Should I test for less, more,etc.’ The assistant features enable you to do that fine tuning.”

TISA also supports ARINC 653, automatically analyzing aerospace programs and mapping detected issues on the common weakness enumeration (CWE) database. In terms of performance, TrustInSoft claims that the new version drastically improves the speed of analyzing complex C++ codebases, with a reported 75% reduction in overall analysis time. 

The Importance of Formal Verification and Static Code Analysis 

Formal verification and static code analysis are both increasingly essential tools in ensuring software security, especially as software complexity and safety-critical applications proliferate. 

Formal verification uses mathematical methods to prove software's correctness, guaranteeing that the software will behave as expected under all possible conditions. In contrast to traditional testing, which checks specific scenarios, formal verification mathematically models all potential behaviors of a system to negate unintended errors or vulnerabilities.

An example of why Formal Verification is important. Image used courtesy of TrustinSoft. (Click image to enlarge)

Static code analysis inspects source code without executing it. This method identifies bugs, security vulnerabilities, and performance bottlenecks early in the development cycle. Unlike dynamic testing, which runs the code to detect issues during execution, static analysis focuses on the structure and logic of the code. It facilitates compliance with coding standards and detects issues such as leaks, race conditions, and overflows before they manifest in runtime.

The software industry is transitioning toward formal verification and static analysis due to the increasing complexity of modern software systems. Meanwhile, regulatory standards such as ISO 26262 and DO-178C demand higher levels of safety assurance and, therefore, have catalyzed the shift toward these analysis methods. Traditional testing and dynamic analysis often fail to cover all possible edge cases, leaving systems vulnerable to rare but potentially catastrophic bugs. Formal methods guarantee more exhaustive coverage.

Automated and Secure Software Verification

As software complexity grows across industries, the need for robust verification methods will only intensify. Tools like TrustInSoft Analyzer offer a glimpse into how formal verification and static code analysis can become the standard in ensuring software reliability and security. This shift toward more automated, precise verification processes will be instrumental in meeting evolving regulatory standards and industry demands. By adopting such advanced methodologies, companies can more effectively mitigate the risk of failures for their software applications.