I have developed, helped in the development, or led the construction of several software tools used in research and industry.
I developed a technique based on model-checking that works with IEC 61131-3 industrial control software. In my PhD thesis I show how automatic test generation for IEC 61131-3 programs, containing both functional and timing information, can be solved as a model checking problem for both code and mutation coverage criteria. The developed technique was implemented by me, Adnan Causevic, Daniel Sundmark and Paul Pettersson in the CompleteTest tool. A commercial version of the tool is developed by Compratio AB.
The only available combinatorial test suite generation tool for IEC 61131-3 control software. SEAFOX supports the generation of test suites using pairwise, base choice and random strategies. For pairwise generation, SEAFOX uses the IPOG algorithm as well as a first pick tie breaker. A developer using SEAFOX can automatically generate test suites needed for a given IEC 61131-3 program after manually providing the input parameter range information based on the defined behaviour written in the specification.
An automatic software complexity measurement tool for IEC 61131-3 FBD programs used in safety critical embedded development. It can measure the Number of Elements, Cyclomatic Complexity Number, Halstead Metrics and Information Flow Metric for block diagrams.
A tool for automatic test generation and test selection using mutation analysis for timed automata and Simulink models via the SIMPAAL tool. The tool is using UPPAAL SMC as the underlying engine.
A tool which provides model-checking of EAST-ADL architectural models with regard to timing and behavioral requirements. It implements an automatic model transformation to UPPAAL PORT timed automata directly from EAST-ADL. The tool has been used in several industrial case studies.
A design tool for behaviour modelling of services based on the REMES language. NetBeans Visual Library API is used to display editable service diagrams with support for graph-oriented models. A textual dynamic service composition language was implemented, together with means to automatically verify the service composition correctness.