|
|
||
|
FMT stands for Formal Methods Toolkit and is a library of functions that facilitate program modeling, static analysis, correctness proofs and automated code generation of programs that need to be correct, especially in the context of safety critical systems.
The meaning of “Formal Methods” in the name is that FMT relies on rigorous mathematical approach for achieving its goals, which allows to ensure the expected program properties by means of logic and proofs instead of inspection or testing. FMT was itself written in the Wolfram programming language and is intended to be used from Mathematica notebooks or from Wolfram scripts. In fact, FMT uses Mathematica for its core computing and symbolic transformation needs.
FMT was created to address several independent concerns frequently found in those software engineering projects that deal with safety-critical systems and which attempt to involve formal methods in their processes - these concerns are outlined end explained below.
A typical software project in the safety-critical domain follows a process that distinguishes separate phases of work or separate kinds of created documents, to represent the logical flow from the user expectations to the final deployed product. The exact number and interactions between such phases depend on the domain, project scale and established engineering culture (which includes commitment to particular work standards), but for the illustration purposes the following major phases can be used:
Further stages, if present, are related to testing, integration, validation and final deployment - and even though they also can be application domains for formal methods, they will rely on formal descriptions created in the three stages listed above (for example, when tests are automatically generated from formal requirements) and therefore are subject to the same concerns.
These three major project stages differ widely in their work methods - to the extent that they require distinct engineering competencies and can be performed by separate teams. In particular, the first stage - the High-Level Requirements stage - involves significant input from the prospective user and is therefore the area where human interaction and negotiation skills can be more important than engineering precision. Interestingly, this is the phase where problem detection and correction has its highest potential benefits and the promise of high investment returns is the reason for which it is very tempting to apply formal methods exactly at this stage.
But it does not seem to work out seamlessly and formal methods developed to target this early, high-level description stage do not seem to gain wider user acceptance.
There can be many different reasons for this, some of them likely related to the fact that committed or potential users who are involved in negotiating new project’s functionality are not necessarily trained mathematicians (they are usually target domain experts) and a typical formal notation might not be comfortable to them. Another possible reason for formal methods not getting attention at this level is that in complex projects, with multiple contractors being involved, it might be too difficult and too early at this stage to standardize on software tools, and using separate tools and notations for dealing with multiple separate engineering teams is not manageable. As a result, more or less structured natural language description is the most frequent choice for High-Level Requirements specification, with all the entailed pros (generic office tools are sufficient to capture the requirements) and cons (possible loss of precision). Those teams that insist on using formal methods at this level of abstraction and collaboration with customer are then forced to translate such natural language requirements descriptions into some selected formal notation, which can be considered to be an additional engineering work that itself induces even more work on verification that the translation was correct and that the two formats are always in sync. It is not always clear whether the prospective gains from the subsequent application of formal methods are indeed worth such an investment.
These concerns seem to be less pronounced at lower level of abstraction, which can be explained by reversing the logic above - at the lower level, the responsibility for the given part is usually owned by a single engineering team and this makes it easier to establish and commit to selected set of software tools. There is no need to translate between artefacts at the same level of abstraction, because the translation from human language to formal notation can be done as part of refinement from High-Level to Low-Level Requirements. Finally, engineers working at lower level, while being less domain-oriented, are typically more comfortable becoming experts in their chosen tools, languages and notations.
The question remains - which of the bottom two levels of abstraction (design or implementation) is more appropriate for the application of formal methods?
There are many existing tools that address different aspects of the project - from the correctness analysis of source code alone (from more or less sophisticated static analysis tools, to proof-enabled extensions of existing programming languages like Frama-C and SPARK for Ada) to design-level modeling and analysis approaches like state machines.
In this context, FMT is positioned somewhere across the design-level and source code. It does this by allowing the engineer to model the program using abstractions that are known from imperative programming languages, like statements, conditions, loops, etc., with a dose of higher-order tools like metaprogramming and code synthesis. The final source code (in Ada, MISRA-C or MISRA-C++) is automatically generated from the model, which allows FMT to be associated with the design-level family of tools - but since FMT is not concerned with concepts like architectural or object-oriented modeling, it does not claim to cover all possible aspects of this project phase.
One of the factors that prevent wider adoption of formal methods is the perceived learning curve that comes from novel or unknown concepts and terminology. Even though formal methods is an established discipline that builds on commonly understood mathematical foundations, the approach to modeling, which is a bridge between system requirements and the actual formal notation, is not necessarily standardized between different tools. This means that concepts like packages, operations, data types, variables and control structures, which are the domain of software engineering, do not always have sufficient or straightforward mapping in the formal notation. Such a notational discontinuity can be treated as an additional and unnecessary cost in the application of any given formal method.
The approach taken by FMT is consistent with the intended level of application, which corresponds to Low-Level Requirements and source code. That is, in order to facilitate modeling at this level of abstraction, FMT directly supports concepts that have straightforward mapping to low-level design elements: packages, data types, data objects, operations, control structures, and so on. This consistency has two benefits - it looks more familiar to software engineers and makes it easier to verify the translation step from the model to the source code, as most of the model constructs have direct and intuitive mapping to source code structures in all supported programming languages. The potential tool qualification effort is also minimized this way.
An important aspect of software tools is their choice of notation and representation - in particular, whether they rely on graphical notations (diagrams) or textual formats.
Both notations can be equally precise and in fact many graphical notations have some equivalent (or even underlying) text forms defined for them.
The choice of notation seems to be important for its users. Even though graphical notations claim higher readability (“A picture is worth a thousand words”), not all engineers subscribe to this idea equally. The reason is that a graphical model is readable as long as it comfortably fits on a single screen (or on a single page) and more complex designs inevitably lose this property, giving way to text formats for their inherent ease of searching, refactoring, reusing or moving fragments around.
Team work is a source of additional concerns, where several engineers might need to update any given file at the same time. Tool support for this kind of work is very mature with regard to text formats, with utilities for computing and displaying differences or patches and for merging updates from multiple authors. Graphical formats suffer from the lack of good and satisfactory support in this area - a picture might be worth a thousand words, but thousands words were sworn as well at engineering desks while merging updates to the same diagram file.
One way to address this concern, without necessarily resigning from the graphical notation whatsoever, is to treat graphical format as a secondary and rendering it from textual descriptions that are then the major focus of the engineering work. In this approach updates are performed on the textual notation (with all benefits resulting from mature support for searching, diffs, patches and merges), while the graphical form, if needed at all, is generated automatically for those who value its readability.
FMT belongs to this group as well. The program is modeled by means of textual notation, familiar to engineers working with any existing imperative programming language, which also makes it easier to reuse such models in scripts (which are textual by their nature) or organize the work of the whole engineering team. Still, various diagrams and analysis results can be generated on demand to visualize many aspects of the model, from grammar trees to call and dependency graphs.
What makes FMT somewhat special in this regard is that FMT models can be created within Mathematica notebooks, interleaved with human-language descriptions, links, diagrams, plots or even interactive elements like buttons and pop-ups to improve the descriptive power of the final design document.
The possibility to automate some or all of the engineering actions is crucial to enable continuous integration. Ideally, only the creative part of engineering should be left (as a privilege, perhaps?) to humans, while allowing tools to automate everything else. Whether tools are trusted or qualified to be left working without supervision is a separate concern (and different domains and engineering teams can have their own policies to address it), but what should be expected from the quality tool is to enable its users to automate at least some of its functions.
There are different ways to approach the concept of automation. If the given tool exists in the form of executable program (like a typical compiler or a static analysis tool), then its automation might rely on external makefiles, batch scripts or even scripts written in one of existing programming languages like Python or Tcl. More elaborate tools that have their own integrated development environments instead embed interpreters of scripting languages and allow users to write simple scripts or plugins to drive or enhance some of their functions.
FMT offers a more radical approach in that it is a library of functions that allow to create, update and verify program models. The library can be imported in the context of Mathematica notebook or a Wolfram script and can be used either interactively (in the Mathematica notebook) or as part of bigger Wolfram programs. This approach might not seem much different from the possibility to invoke an external tool from the Python script, unless it is realised that FMT itself relies on Mathematica for its own operation. This means that the integration between the tool and the scripting platform is the highest possible, enabling advanced features like custom hooks and callbacks or metaprogramming with symbols expanding automatically while the model is being developed or used.
FMT is an open-source toolkit in the sense that its implementation is open to inspection and improvement by all interested parties. The availability of complete source code of all FMT packages is not only a natural result of Wolfram being a scripting language, it is also an intended property that should give potential users a confidence that the tool itself was designed and developed with good sense of engineering craftsmanship and that its internal algorithms do not hide any intentional surprises. A potential for ensuring service continuity is also an important factor for those users who consider the possible authorship and commitment changes as a long-term risk.
It is important to note that even though FMT is an open-source library, it requires Mathematica as a run-time environment, which itself is a closed-source product. Over 30 years of its continuous development and wide deployment in both academia and industry provide the credibility for those who need to consider the run-time platform in their risk assessments.
The Formal Methods Toolkit was created for those engineers who would like to benefit from the power of Mathematica as a universal computing platform and employ its capabilities in the area of software engineering. Applying strict mathematical rigour in software design on one side and unleashing the creativity and productivity that come from existing features of Mathematica on the other side, can offer a unique combination of facilities that a mature software engineering team can benefit from.
FMT is for those engineers who are not satisfied with traditional verification techniques that rely on run-time testing only and who would like to incorporate formal methods in their work in a way that has manageable scope of application, is conceptually familiar, configuration-management-friendly and gives unlimited automation capabilities.
Next: Installing FMT
See also Table of Contents.