Collaboration, conferences and competition for FAIR formal models

Com­put­er sci­en­tist and 4TU.ResearchData advo­cate from the Uni­ver­si­ty of Twente, Arnd Hart­manns, shares ways of devel­op­ing meth­ods and tools that are find­able, acces­si­ble, inter­op­er­a­ble and reusable. 

Arnd explains the impor­tance of devel­op­ing tools and algo­rithms to test the robust­ness, reli­a­bil­i­ty and repro­ducibil­i­ty of soft­ware and hard­ware designs. “To con­firm the safe­ty and secu­ri­ty of high-integri­ty sys­tems, it’s crit­i­cal to check that all aspects of a sys­tem oper­ate as expect­ed at the spec­i­fi­ca­tion stage.”

“Using prob­a­bilis­tic mod­el­ling, it’s pos­si­ble to pre­dict whether or not a sys­tem will oper­ate cor­rect­ly under var­i­ous con­di­tions,” He adds. “This means that prob­lems can be solved and mit­i­ga­tion mea­sures can be put in place to pre­vent sys­tem fail­ure before imple­men­ta­tion.”

Val­i­dat­ing the work of oth­ers

At the Uni­ver­si­ty, Arnd works with researchers from diverse dis­ci­plines to ver­i­fy their design sys­tems. By way of exam­ple, Pro­fes­sor Mar­iëlle Stoelin­ga uses for­mal mod­els, specif­i­cal­ly machine learn­ing and algo­rithms for fault tree analy­sis, in projects that aim to improve the Dutch rail­road infra­struc­ture (Read more about her Sequoia, For­maSig and Pri­maV­era projects).

Sim­i­lar­ly, Asso­ciate Pro­fes­sor Rom Langer­ak applies com­pu­ta­tion­al mod­el­ling tech­niques to clin­i­cal med­i­cine. His recent pub­li­ca­tion employs the for­mal mod­el of timed automa­ta using the UPPAAL tool to eval­u­ate tooth wear mon­i­tor­ing in den­tistry. 

‘Mod­est’ col­lab­o­ra­tions

Arnd’s col­lab­o­ra­tive efforts extend far beyond his own research insti­tu­tion. His ‘Mod­est Toolset’ for quan­ti­ta­tive mod­el­ling and ver­i­fi­ca­tion is avail­able to researchers around the world. 

In Ger­many, Mod­est was used to cer­ti­fy com­pli­ance with the Ener­gy­Bus stan­dard for light elec­tric vehi­cle com­po­nents; in Italy, it was used to analyse the secu­ri­ty of cyber-phys­i­cal sys­tems; and, in the U.S. it was used to eval­u­ate pow­er sup­ply noise in net­work-on-chip designs. 

To ensure that Mod­est is inter­op­er­a­ble with oth­er tools, Arnd and his col­lab­o­ra­tors at RWTH Aachen Uni­ver­si­ty and the Insti­tute of Soft­ware Chi­nese Acad­e­my of Sci­ences devel­oped The JANI Spec­i­fi­ca­tion; a stan­dard mod­el inter­change for­mat and tool inter­ac­tion pro­to­col. 

“JANI con­verts mod­els spec­i­fied in the Mod­est mod­el­ling lan­guage to a JSON data for­mat which is easy to use, exten­si­ble and sup­port­ed by numer­ous user inter­faces.” Arnd con­tin­ues, “The ulti­mate goal of JANI is to sim­pli­fy tool devel­op­ment and encour­age research coop­er­a­tion in mod­el ver­i­fi­ca­tion.”

Arti­facts as FAIR repli­ca­tion pack­ages

Anoth­er way to encour­age research coop­er­a­tion in the field of Com­put­er Sci­ence is through the gen­er­a­tion and eval­u­a­tion of arti­facts. 

Arti­facts are essen­tial­ly ‘repli­ca­tion pack­ages’ that con­tain the full details of exper­i­ments con­duct­ed as part of a sci­en­tif­ic pub­li­ca­tion. They include soft­ware, datasets or machine-check­able proofs that sub­stan­ti­ate claims made in a pub­li­ca­tion and make them repro­ducible by oth­ers.

“For an arti­fact to be FAIR, the tool bina­ry or source code, its doc­u­men­ta­tion, input files required for tool eval­u­a­tion, and a con­fig­u­ra­tion file or doc­u­ment that describes the exper­i­men­tal para­me­ters must be made avail­able,” says Arnd.

Arnd’s arti­facts are pub­li­cal­ly avail­able in the 4TU.ResearchData repos­i­to­ry. He explains the advan­tages of pub­lish­ing his arti­facts. 

“First­ly, oth­ers can eval­u­ate the results I present in my pub­li­ca­tions by re-run­ning my exper­i­ment. Sec­ond­ly, oth­ers can reuse and devel­op my meth­ods to ben­e­fit their own research. Third­ly, I can reuse and build upon the meth­ods I devel­oped years ago myself!” 

Con­fer­ences that dri­ve cul­tur­al change

Impor­tant con­fer­ences in the field, such as the Inter­na­tion­al Con­fer­ence on Com­put­er-Aid­ed Ver­i­fi­ca­tion (CAV) and the Inter­na­tion­al Con­fer­ence on Tools and Algo­rithms for the Con­struc­tion and Analy­sis of Sys­tems (TACAS), have made arti­fact eval­u­a­tion com­pul­so­ry to dri­ve a cul­ture change towards more repro­ducible research. 

Arnd was co-chair of the Arti­fact Eval­u­a­tion Com­mit­tee for TACAS in 2018 and 2020. This year, the com­mit­tee man­dat­ed that tool and tool demon­stra­tion papers must be accom­pa­nied by an arti­fact for eval­u­a­tion by the com­mit­tee at the point of sub­mis­sion. 

From this, the com­mit­tee can assess how the tool oper­ates; what the exact exper­i­men­tal para­me­ters were, and whether the results in the paper can be inde­pen­dent­ly con­firmed.

Arti­facts that sat­is­fy cri­te­ria for con­sis­ten­cy, replic­a­bil­i­ty, com­plete­ness and ease of use are accept­ed and the papers stamped with a ‘seal of approval’ as they receive a badge endorse­ment that can be dis­played on the title page upon offi­cial pub­li­ca­tion. 

Com­pe­ti­tions to build the com­mu­ni­ty

When it comes to reward and recog­ni­tion for good research prac­tice, per­haps there’s some­thing to be learned from the ver­i­fi­ca­tion com­pe­ti­tions host­ed by TACAS and sim­i­lar con­fer­ences. 

In the field of ver­i­fi­ca­tion tech­nol­o­gy, com­pe­ti­tions and awards pro­vide a suit­able means for objec­tive eval­u­a­tion and com­par­i­son between for­mal meth­ods and tools against a com­mon set of bench­marks. 

The ‘Dis­tin­guished Arti­fact Awards’ are a good exam­ple. For trans­paren­cy, all eval­u­at­ed arti­facts are pub­lished, but those that are excep­tion­al­ly well-pack­aged, well-designed and well-doc­u­ment­ed win the award.

Arnd reflects on TOOLympics 2019, an event that host­ed 16 com­pe­ti­tions as part of the cel­e­bra­tions that marked the 25th anniver­sary of TACAS. 

“Com­pe­ti­tions help to advance research; they bring the com­mu­ni­ty togeth­er, raise aware­ness and stim­u­late knowl­edge exchange. What’s more, researchers have a unique oppor­tu­ni­ty to test their pro­to­types in prac­tice, com­pare state of the art tech­nolo­gies, cel­e­brate progress and receive recog­ni­tion for their sci­en­tif­ic con­tri­bu­tion.” 

Whilst con­tests and prizes have become an inte­gral part of the sci­en­tif­ic method for com­put­er sci­en­tists, per­haps we can be inspired to inte­grate sim­i­lar incen­tives to reward FAIR and repro­ducible research in oth­er research dis­ci­plines. What do you think?

Do you have any ideas to fol­low up on this sto­ry? Please share them with us!

Writ­ten by Con­nie Clare (4TU.ResearchData)
Cov­er image illus­trat­ed by Con­nie Clare (4TU.ResearchData)