Tool Seminar:2006 Tool List
From Dependability
| Overview | | Schedule | | Syllabus | | 2006 Project Guidelines | | Tool List | | Editing Guidelines |
We have compiled a set of tools from which you may choose one for your project. Many of the model checkers are open source products and are freely available. The Model-Based Development tools, on the other hand, are industry products and have been made available thanks to the generosity of the tool vendor.
Model Checkers
Contents |
Spin
Spin is a popular open-source software tool, used by thousands of people worldwide, that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. In April 2002 the tool was awarded the prestigious System Software Award for 2001 by the ACM.
KRONOS
KRONOS is a tool developed with the aim to verify complex real-time systems. In KRONOS, components of real-time systems are modeled by timed automata and the correctness requirements are expressed in the real-time temporal logic TCTL. KRONOS checks whether a timed automaton satisfies a TCTL-formula. KRONOS is freely distributed to academic institutions for non-profit use.
Uppaal
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark.
BLAST
BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. Blast uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on-the-fly, and only to the required precision. The BLAST project is supported by the National Science Foundation.
Java Pathfinder
Java PathFinder (JPF) is a system to verify executable Java bytecode programs. In its basic form, it is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Unlike traditional debuggers, JPF reports the entire execution path that leads to a defect. JPF is especially well-suited to finding hard-to-test concurrency defects in multithreaded programs.
SLAM
Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we’re building tools that can do actual proof about the software and how it works in order to guarantee the reliability.
Model-Based Development
Perfect Developer
Perfect Developer empowers your organisation to develop components, classes and systems guaranteed to behave according to precise specifications and meet user requirements. Perfect Developer encourages an object-oriented development style but also supports a procedural style. It can be used for specification and design only or can generate final code in a choice of modern programming languages. Perfect Developer is intended for any organization that carries out software development to high standards, but is particularly valuable for aerospace and other safety-critical software development and for developing mission-critical applications. It is also suitable for use by universities and colleges in teaching the principles of sound software development or the Verified Design By Contract method.
Simulink
Simulink is a platform for multidomain simulation and Model-Based Design for dynamic systems. It provides an interactive graphical environment and a customizable set of block libraries, and can be extended for specialized applications.
STATEMATE
Statemate enables engineers to rapidly design and validate complex systems level products through a unique combination of graphic modeling, simulation, code generation, documentation generation, and test plan definition. As a result, Statemate has emerged as the standard for high-end embedded systems development within the medical, automotive, aerospace, and defense industries.
Rhapsody
The newest release of Rhapsody, version 6.1, offers a rich feature set to users with key enabling technologies that empower designers and developers to use SysML, DoDAF, CORBA and in a natural, easy-to-use tool environment. Loaded with enhancements and new features to make a seamless and efficient environment for systems, software and testability, the new tool family represents a “best of breed” solution to users.
SCR Toolset
In previous research funded by NRL's 6.1 Base Program, Code 5546 has developed a comprehensive formal model and numerous algorithms and other formal techniques for developing complete, consistent and correct software requirements specifications. In this new 6.1 program, Code 5546 is undertaking new research that will produce a formal foundation for transforming a verified, validated requirements specification into a reliable, provably correct, efficient software implementation. The formal foundation is intended to allow the development of user-friendly automated support for the tranformation process. The result will be a tool set and methodology that can support the full software development cycle for developers of Navy and other high assurance applications.
SCADE Suite
Our technology and methodology begins with the system requirements allocated to software from which we produce the formal software specification (software requirements). This creates a "contract" between the systems designer and the software architect. It is this contract which enables SCADE to become a communication vehicle between these two functions and lays the foundation by which SCADE can be used as a signoff document.