Publications

Here is a selection of my publications.

You can also find externally curated collections on
DBLP, Google Scholar and ResearchGate.

2018 (5)

ML4CREST: Machine Learning for CPS Models.
Stefan Klikovits, Auélien Coet and Didier Buchs
In 2nd International Workshop on Model Driven Engineering for the Internet-of-Things (MDE4IOT), Copenhagen, 2018, 2018.

 Abstract 

Models of small CPS and IoT applications often use approximated values that describe physical system behaviour. Physical resources, such as electricity consumption and heating power, have to be estimated, since many off-the-shelf components lack the required descriptions. Controllers which are based on these approximations can hence use imprecise models, perform misleading simulation, and cause damaged systems and financial loss. In this paper we present ML4CREST, a machine learning approach to automatically calibrate models using sensor measurements. We show that our approach is well-suited for the calibration of the flow rates within an automated watering system, which allows precise simulation and prevents spillage.

 PDF   Slides 

 Bibtex 

@InProceedings{Klikovits:MDE4IOT:ML4CREST, title = {{ML4CREST}: Machine Learning for CPS Models}, author = {Stefan Klikovits and Aur\'{e}lien Coet and Didier Buchs}, booktitle = {2nd International Workshop on Model Driven Engineering for the Internet-of-Things (MDE4IOT), Copenhagen, Denmark, October 15, 2018. Proceedings}, year = {2018}, }

CREST - A DSL for Reactive Cyber-Physical Systems.
Stefan Klikovits, Alban Linard and Didier Buchs
In Proceedings of 10th System Analysis and Modeling Conference (SAM 2018), October 15-16, Copenhagen, Denmark/, pp 29-45, 2018.

 Abstract 

This article presents CREST, a novel domain-specific language for the modelling of cyber-physical systems. CREST is designed for the simple and clear modelling, simulation and verification of small-scale systems such as home and office automation, smart gardening systems and similar. The language is designed to model the flow of resources throughout the system. It features synchronous system evolution and reactive behaviour. CREST's formal semantics allow real-valued time advances and the modelling of timed system evolution. The continuous time concept permits the precise simulation of future system behaviour by automatically calculating next transition times. We present CREST in a practical manner, and elaborate on the Python-based DSL implementation and simulator.

 PDF   Slides   Link   DOI 

 Bibtex 

@inproceedings{Klikovits:SAM18:CREST, title = {{{CREST}} - {{A DSL}} for {{Reactive Cyber}}-{{Physical Systems}}}, isbn = {978-3-030-01042-3}, booktitle = {10th System {{Analysis}} and {{Modeling}} {{Conference}} ({{SAM2018}}). {{Languages}}, {{Methods}}, and {{Tools}} for {{Systems Engineering}}}, publisher = {{Springer International Publishing}}, author = {Klikovits, Stefan and Linard, Alban and Buchs, Didier}, editor = {Khendek, Ferhat and Gotzhein, Reinhard}, year = {2018}, pages = {29-45}, doi = {10.1007/978-3-030-01042-3_3} }

Petri Sport: A Sport for Petri Netters.
Stefan Klikovits, Alban Linard, Dimitri Racordon and Didier Buchs
In Proceedings of Petri Nets and Software Engineering. International Workshop, PNSE'18, Bratislava, Slovakia, June 25-26, 2018, pp 35-56, 2018.

 Abstract 

Petri nets are a family of formalisms dedicated to the representation of concurrent systems. Their strength is the compact modeling of complex behaviors using very simple rules. Despite this simplicity, many teachers observe that students often require a lot of exposure and numerous exercises to truly understand the semantics of Petri nets. In order to speed up this learning process and provide a different attack angle, we propose Petri sport, a fun game based upon the Petri net formalism. In Petri sport, players aim to gather points by moving across a Petri net-shaped playing field and "firing" transitions. A clock-based play style supports a structured game advance while at the same time it encourages players to move fast. As the playing field is shaped like a Petri net, it is possible to challenge a player's movement speed, intellectual capabilities, as well as team coordination and communication. The difficulty level of Petri sport is based on the choice of playing field. This allows for adaptation in order to best fit the competitors' age, experience and/or physical fitness level.

 PDF   Slides   Github 

 Bibtex 

@InProceedings{Klikovits:PNSE18:PetriSport, title = {{Petri} Sport: A Sport for {Petri} Netters}, pages = {35--56}, author = {Stefan Klikovits and Alban Linard and Dimitri Racordon and Didier Buchs}, year = 2018, booktitle = {Petri Nets and Software Engineering. International Workshop, PNSE'18, Bratislava, Slovakia, June 25-26, 2018. Proceedings}, editor = {Moldt, Daniel and Kindler, Ekkart and R{\"o}lke, Heiko}, series = {CEUR Workshop Proceedings}, publisher = {CEUR-WS.org}, volume = {2138} }

A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning.
Didier Buchs, Stefan Klikovits, Alban Linard, Romain Mencattini and Dimitri Racordon
In Proceedings of Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24-29, pp 385-395, 2018.

 Abstract 

This paper introduces mcc4mcc, the Model Checker Collection for the Model Checking Contest, a tool that wraps multiple model checking solutions, and applies the most appropriate one based on the characteristics of the model it is given. It leverages machine learning algorithms to carry out this selection, based on the results gathered from the 2017 edition of the Model Checking Contest, an annual event in which multiple tools compete to verify different properties on a large variety of models. Our approach brings two important contributions. First, our tool offers the opportunity to further investigate on the relation between model characteristics and verification techniques. Second, it lays out the groundwork for a unified way to distribute model checking software using virtual containers.

 PDF   Slides   DOI 

 Bibtex 

@inproceedings{DBLP:conf/apn/BuchsKLMR18, author = {Didier Buchs and Stefan Klikovits and Alban Linard and Romain Mencattini and Dimitri Racordon}, title = {A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning}, booktitle = {Application and Theory of Petri Nets and Concurrency - 39th International Conference, {PETRI} {NETS} 2018, Bratislava, Slovakia, June 24-29, 2018, Proceedings}, pages = {385--395}, year = {2018}, doi = {10.1007/978-3-319-91268-4_21} }

CREST Formalization.
Stefan Klikovits, Alban Linard and Didier Buchs
In Technical Report, Software Modeling and Verification Group, University of Geneva, 2018.

 Abstract 

CREST is a novel modelling language for the definition of Continuous-time, REactive SysTems. This domain-specific language (DSL) targets small cyber-physical systems (CPS) such as home automation systems. While CREST is a graphical language and its systems can be visualised as CREST diagrams, the main form of use is as internal DSL for the Python general purpose programming language. Nevertheless, CREST systems are based on a formal structure and semantics. This report provides this formalisation and elaborates on the design choices that have been made.

 PDF   DOI 

 Bibtex 

@techreport{Klikovits:CRESTFormalization, author = {Stefan Klikovits and Alban Linard and Didier Buchs}, title = {{CREST} Formalization}, institution = {Software Modeling and Verification Group, University of Geneva}, doi = {10.5281/zenodo.1284561}, year = {2018} }

2017 (4)

Towards Lanuguage Independent (Dynamic) Symbolic Execution.
Stefan Klikovits, Manuel Gonzalez-Berges and Didier Buchs
In In Proceedings of the 24th PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, pp 50-53, 2017.

 Abstract 

Symbolic execution is well-known for its capability to produce high-coverage test suites for software source code. So far, most tools are created to support a specific language. This paper elaborates on performing language independent symbolic execution and three ways to achieve it. We describe the use of one approach to perform dynamic symbolic execution using translation of a proprietary language and show the results of the tool execution on a real-life codebase.

 PDF   Slides   DOI 

 Bibtex 

@inproceedings{klikovits:2017:minisy, author = {Stefan Klikovits and Manuel Gonzalez{-}Berges and Didier Buchs}, title = {Towards Lanuguage Independent (Dynamic) Symbolic Execution}, year = {2017}, booktitle = {Proceedings of the 24th PhD Mini-Symposium}, pages = {50--53}, isbn = {978-963-313-243-2}, venue = {Budapest, Hungary}, url = {https://doi.org/10.5281/zenodo.291899}, publisher = {{Budapest University of Technology and Economics, Department of Measurement and Information Systems}}, doi = {10.5281/zenodo.291899}, }

The Experiment Model and Validity Frame in M&S.
Joachim Denil, Stefan Klikovits, Pieter J. Mosterman, Antonio Vallecillo and Hans Vangheluwe
In Proceedings of the Symposium on Theory of Modeling & Simulation: DEVS Integrative M&S Symposium, Virginia Beach, Virginia, USA, April 23-26 , pp 109-120, 2017.

 Abstract 

Modelling and Simulation approaches use system models to conduct simulation experiments. Experimental frames have been applied in this context to formally define a system's context. During the creation of an experimental frame for a simple spring model it becomes clear that experimental frames in their current definition lack certain properties and omit relevant information. Our approach describes the process of capturing the context of models and systems to provide truly reproducible experiment descriptions. The information, captured as experimental setups, can then be used for different purposes and in different scenarios, in particular for checking the validity of a model, the discovery of suitable models for the design of a system, and for calibrating models.

 PDF   Link 

 Bibtex 

@inproceedings{denil:2017:springsim, author = {Joachim Denil and Stefan Klikovits and Pieter J. Mosterman and Antonio Vallecillo and Hans Vangheluwe}, title = {The Experiment Model and Validity Frame in M\&S}, year = {2017}, booktitle = {Proceedings of the Symposium on Theory of Modeling \& Simulation}, series = {TMS/DEVS '17}, pages = {109--120}, isbn = {ISBN: 978-1-5108-3823-9}, venue = {Virginia Beach, Virginia, USA}, url = {http://scs.org/wp-content/uploads/2017/06/27_Final_Manuscript.pdf}, }

Modeling Frames.
Stefan Klikovits, Joachim Denil, Alexandre Muzy and Rick Salay
In 14th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa} 2017), 19 September, Austin, TX, USA, pp 315-320, 2017.

 Abstract 

Modeling activities such as calibration, verification and validation are often executed in under-specified environments. This hinders reproducibility, reduces re-usability and generally decreases the modeling precision and quality. This paper describes a framework for the definition of model frames. Model frames capture the context an activity/model is executed in and facilitate re-use, replacement, validation and verification of models. We show the application of the frames approach onto a real-world example, introduce several kinds of frames and show their application on this case study.

 PDF   Slides 

 Bibtex 

@inproceedings{DBLP:conf/models/KlikovitsDMS17, author = {Stefan Klikovits and Joachim Denil and Alexandre Muzy and Rick Salay}, title = {Modeling Frames}, booktitle = {14th Workshop on {Model-Driven Engineering, Verification and Validation} {(MoDeVVa} 2017), 19 September 2017, Austin, TX, USA}, pages = {315--320}, year = {2017} }

CREST - A Continuous, REactive SysTems DSL.
Stefan Klikovits, Alban Linard and Didier Buchs
In 5th International Workshop on the Globalization of Modeling Languages (GEMOC} 2017, 19 September, Austin, TX, USA, pp 286-291, 2017.

 Abstract 

The advance of cyber-physical systems in everyday life requires powerful modeling capabilities. Existing formalisms often have severe limitations and require complicated notations. In this paper we introduce CREST, a domain-specific language for modeling entity behavior and resource transfers in CPS. CREST aims to support CPS architects through clarity, comprehensiveness and analyzability.

 PDF   Slides 

 Bibtex 

@inproceedings{DBLP:conf/models/KlikovitsLB17, author = {Stefan Klikovits and Alban Linard and Didier Buchs}, title = {{CREST} - {A} Continuous, REactive SysTems {DSL}}, booktitle = {5th International Workshop on the {Globalization of Modeling Languages} {(GEMOC} 2017), 19 September 2017, Austin, TX, USA}, pages = {286--291}, year = {2017} }

2016 (1)

Automated Test Case Generation for the CTRL Programming Language Using Pex: Lessons Learned.
Stefan Klikovits, David P. Y. Lawrence, Manuel Gonzalez-Berges and Didier Buchs
In Proceedings of Software Engineering for Resilient Systems - 8th International Workshop, SERENE 2016, Gothenburg, Sweden, September 5-6, 2016, Proceedings, pp 117-132, 2016.

 Abstract 

Over the last decade code-based test case generation techniques such as combinatorial testing or dynamic symbolic execution have seen growing research popularity. Most algorithms and tool implementations are based on finding assignments for input parameter values in order to maximise the execution branch coverage. In this paper we first present ITEC, a tool for automated test case generation in CTRL, as well as initial results of test cases executions on one of CERN’s SCADA frameworks. Our tool relies on Microsoft’s Pex for its code exploration. For the purpose of using this existing test generation tool, we have to translate the proprietary CTRL code into C#, one of Pex’s operating languages. Our main contribution lies in detailing a formal foundation for this step through source code decomposition and anonymization. We then propose a quality measure that is used to determine our confidence into the translation and the generated test cases.

 PDF   Slides   DOI 

 Bibtex 

@inproceedings{DBLP:conf/serene/KlikovitsLGB16, author = {Stefan Klikovits and David P. Y. Lawrence and Manuel Gonzalez{-}Berges and Didier Buchs}, title = {Automated Test Case Generation for the {CTRL} Programming Language Using Pex: Lessons Learned}, booktitle = {Software Engineering for Resilient Systems - 8th International Workshop, {SERENE} 2016, Gothenburg, Sweden, September 5-6, 2016, Proceedings}, pages = {117--132}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-45892-2_9}, doi = {10.1007/978-3-319-45892-2_9}, }

2015 (1)

Considering Execution Environment Resilience: A White-Box Approach.
Stefan Klikovits, David P. Y. Lawrence, Manuel Gonzalez-Berges and Didier Buchs
In Proceedings of Software Engineering for Resilient Systems - 7th International Workshop, SERENE 2015, Paris, France, September 7-8, 2015, 2015.

 Abstract 

Over the last decade code-based test case generation techniques such as combinatorial testing or dynamic symbolic execution have seen growing research popularity. Most algorithms and tool implementations are based on finding assignments for input parameter values in order to maximise the execution branch coverage. Only few of them consider dependencies from outside the Code Under Test’s scope such as global variables, database values and subroutine calls as influences to the execution path. In order to fully test all possible scenarios these dependencies have to be taken into account for the test input generation. This paper introduces ITEC, a tool for automated test case generation to support execution environment resilience in large-scaled, complex systems. One of ITEC’s corner stones is a technique called semi-purification, a source code transformation technique to overcome limitations of existing tools and to set up the required system state for software testing.

 PDF   Slides   DOI 

 Bibtex 

@inproceedings{DBLP:conf/serene/KlikovitsLGB15, author = {Stefan Klikovits and David P. Y. Lawrence and Manuel Gonzalez{-}Berges and Didier Buchs}, title = {Considering Execution Environment Resilience: {A} White-Box Approach}, booktitle = {Software Engineering for Resilient Systems - 7th International Workshop, {SERENE} 2015, Paris, France, September 7-8, 2015. Proceedings}, pages = {46--61}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-23129-7_4}, doi = {10.1007/978-3-319-23129-7_4}, }

2011 (1)

Multi-platform SCADA GUI Regression Testing at CERN.
Paul C. Burkimsher, Manuel Gonzalez-Berges and Stefan Klikovits
In Proceedings of the 13th International Conference on Accelerator and Large Experimental Physics Control Systems, 2011.

 Abstract 

The JCOP Framework is a toolkit used widely at CERN for the development of industrial control systems in several domains (i.e. experiments, accelerators and technical infrastructure). The software development started 10 years ago and there is now a large base of production systems running it. For the success of the project, it was essential to formalize and automate the quality assurance process. The paper will present the overall testing strategy and will describe in detail mechanisms used for GUI testing. The choice of a commercial tool (Squish) and the architectural features making it appropriate for our multi-platform environment will be described. Practical difficulties encountered when using the tool in the CERN context are discussed as well as how these were addressed. In the light of initial experience, the test code itself has been recently reworked in OO style to facilitate future maintenance and extension. The paper concludes with a description of our initial steps towards incorporation of full-blown Continuous Integration (CI) support.

 PDF   Slides   Link 

 Bibtex 

@inproceedings{burkimsher:2011:icalepcs, author = {Paul C. Burkimsher and Manuel Gonzalez{-}Berges and Stefan Klikovits}, title = {Multi-platform SCADA GUI Regression Testing at CERN}, booktitle = {Proceedings of the 13th International Conference on Accelerator and Large Experimental Physics Control Systems}, year = {2011}, venue = {Grenoble, France}, publisher = {JACoW} }