Assistant Professor, Arnd Hartmanns, works within the faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente.
His research on Formal Methods and Tools involves the development of mathematical models to verify complex real-time designs.
Arnd explains the importance of developing tools and algorithms to test the robustness, reliability and reproducibility of software and hardware designs. “To confirm the safety and security of high-integrity systems, it’s critical to check that all aspects of a system operate as expected at the specification stage.”
“Using probabilistic modelling, it’s possible to predict whether or not a system will operate correctly under various conditions,” He adds. “This means that problems can be solved and mitigation measures can be put in place to prevent system failure before implementation.”
Validating the work of others
At the University, Arnd works with researchers from diverse disciplines to verify their design systems. By way of example, Professor Mariëlle Stoelinga uses formal models, specifically machine learning and algorithms for fault tree analysis, in projects that aim to improve the Dutch railroad infrastructure (Read more about her Sequoia, FormaSig and PrimaVera projects).
Similarly, Associate Professor Rom Langerak applies computational modelling techniques to clinical medicine. His recent publication employs the formal model of timed automata using the UPPAAL tool to evaluate tooth wear monitoring in dentistry.
Arnd’s collaborative efforts extend far beyond his own research institution. His ‘Modest Toolset’ for quantitative modelling and verification is available to researchers around the world.
In Germany, Modest was used to certify compliance with the EnergyBus standard for light electric vehicle components; in Italy, it was used to analyse the security of cyber-physical systems; and, in the U.S. it was used to evaluate power supply noise in network-on-chip designs.
To ensure that Modest is interoperable with other tools, Arnd and his collaborators at RWTH Aachen University and the Institute of Software Chinese Academy of Sciences developed The JANI Specification; a standard model interchange format and tool interaction protocol.
“JANI converts models specified in the Modest modelling language to a JSON data format which is easy to use, extensible and supported by numerous user interfaces.” Arnd continues, “The ultimate goal of JANI is to simplify tool development and encourage research cooperation in model verification.”
Artifacts as FAIR replication packages
Another way to encourage research cooperation in the field of Computer Science is through the generation and evaluation of artifacts.
Artifacts are essentially ‘replication packages’ that contain the full details of experiments conducted as part of a scientific publication. They include software, datasets or machine-checkable proofs that substantiate claims made in a publication and make them reproducible by others.
“For an artifact to be FAIR, the tool binary or source code, its documentation, input files required for tool evaluation, and a configuration file or document that describes the experimental parameters must be made available,” says Arnd.
“Firstly, others can evaluate the results I present in my publications by re-running my experiment. Secondly, others can reuse and develop my methods to benefit their own research. Thirdly, I can reuse and build upon the methods I developed years ago myself!”
Conferences that drive cultural change
Important conferences in the field, such as the International Conference on Computer-Aided Verification (CAV) and the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), have made artifact evaluation compulsory to drive a culture change towards more reproducible research.
Arnd was co-chair of the Artifact Evaluation Committee for TACAS in 2018 and 2020. This year, the committee mandated that tool and tool demonstration papers must be accompanied by an artifact for evaluation by the committee at the point of submission.
From this, the committee can assess how the tool operates; what the exact experimental parameters were, and whether the results in the paper can be independently confirmed.
Artifacts that satisfy criteria for consistency, replicability, completeness and ease of use are accepted and the papers stamped with a ‘seal of approval’ as they receive a badge endorsement that can be displayed on the title page upon official publication.
Competitions to build the community
When it comes to reward and recognition for good research practice, perhaps there’s something to be learned from the verification competitions hosted by TACAS and similar conferences.
In the field of verification technology, competitions and awards provide a suitable means for objective evaluation and comparison between formal methods and tools against a common set of benchmarks.
The ‘Distinguished Artifact Awards’ are a good example. For transparency, all evaluated artifacts are published, but those that are exceptionally well-packaged, well-designed and well-documented win the award.
Arnd reflects on TOOLympics 2019, an event that hosted 16 competitions as part of the celebrations that marked the 25th anniversary of TACAS.
“Competitions help to advance research; they bring the community together, raise awareness and stimulate knowledge exchange. What’s more, researchers have a unique opportunity to test their prototypes in practice, compare state of the art technologies, celebrate progress and receive recognition for their scientific contribution.”
Whilst contests and prizes have become an integral part of the scientific method for computer scientists, perhaps we can be inspired to integrate similar incentives to reward FAIR and reproducible research in other research disciplines. What do you think?
Do you have any ideas to follow up on this story? Please share them with us!