Publications

Here is a selection of my publications. You can also find externally curated collections on DBLP, Google Scholar and ResearchGate.

2019 (4)

Stefan Klikovits. PhD Thesis: A Domain-Specific Language Approach To Hybrid CPS Modelling. In: Archive Ouverte, University of Geneva. 2019.

PDF Link DOI
Bibtex
@phdthesis{klikovits_phdthesis_2019,
    author = {Klikovits, Stefan},
    title = {A Domain-Specific Language Approach To Hybrid CPS Modelling},
    year = {2019},
    school = {University of Geneva, Switzerland},
    url = {https://archive-ouverte.unige.ch/unige:121355},
    doi = {10.13097/archive-ouverte/unige:121355}
}

Stefan Klikovits et al. State-of-the-art on Current Formalisms used in Cyber-Physical Systems Development. In: COST IC1404 WG1 Deliverable WG1.1. 2019.

DOI
Bibtex
@misc{klikovits_stefan_2019_2538711,
  author = {Klikovits, Stefan and Al-Ali, Rima 
      and Amrani, Moussa and Barisic, Ankica 
      and Barros, Fernando and Blouin, Dominique 
      and Borde, Etienne and Buchs, Didier 
      and Giese, Holger and Goulao, Miguel 
      and Iacono, Mauro and Leon, Florin 
      and Navarro, Eva and Pelliccione, Patrizio 
      and Vanherpen, Ken},
  title = {{COST IC1404 WG1 Deliverable WG1.1: 
      State-of-the-art on Current Formalisms used 
      in Cyber-Physical Systems Development}},
  month = jan,
  year = 2019,
  doi = {10.5281/zenodo.2533455},
  url = {https://doi.org/10.5281/zenodo.2533455}
}

Rima Al-Ali et al. Framework to Relate / Combine Modeling Languages and Techniques. In: COST IC1404 WG1 Deliverable WG1.2. 2019.

DOI
Bibtex
@misc{al_ali_rima_2019_2527577,
  author = {Al-Ali, Rima and Amrani, Moussa and 
      Bandyopadhyay, Soumyadip and Barisic, Ankica 
      and Barros, Fernando and Blouin, Dominique 
      and Erata, Ferhat and Giese, Holger 
      and Iacono, Mauro and Klikovits, Stefan 
      and Navarro, Eva and Pelliccione, Patrizio 
      and Taveter, Kuldar and Tekinerdogan, Bedir 
      and Vanherpen, Ken},
  title = {{COST IC1404 WG1 Deliverable WG1.2: 
      Framework to Relate / Combine 
      Modeling Languages and Techniques}},
  month = jan,
  year = 2019,
  doi = {10.5281/zenodo.2527576},
  url = {https://doi.org/10.5281/zenodo.2527576}
}

Didier Buchs, Stefan Klikovits and Alban Linard. Petri Nets: A Formal Language to Specify and Verify Concurrent Non-Deterministic Event Systems. In: P. Carreira and V. Amaral and H. Vangheluwe (eds.) Foundations of Multi-Paradigm Modelling for Cyber-Physical Systems. 2019.

Abstract
The study of concurrent and parallel systems has been a challenging research domain  within cyber-physical systems community. This chapter provides a pragmatic introduction to the creation and analysis of such system models using the popular Petri nets  formalism. Petri nets is a formalism that convinces through its simplicity and  applicability. We offer an overview of the most important Petri nets concepts,  analysis techniques and model checking approaches. Finally, we show the use of  so-called High-level Petri nets for the representation of complex data structures  and functionality and present a novel research approach that allows the use of Petri nets inside Functional Mock-up Units and cyber-physical system models.
Bibtex
@inbook{Klikovits:2019:mpm4cps:foundationsbook,
  author={Didier Buchs and Stefan Klikovits and Alban Linard},
  title={{Petri Nets: A Formal Language to Specify and Verify Concurrent Non-Deterministic Event Systems}}, 
  booktitle= {{Foundations of Multi-Paradigm Modelling for Cyber-Physical Systems}}, 
  editor = {P. Carreira and V. Amaral and H. Vangheluwe}, 
  publisher= {Springer},
  year= 2019,
  note = {(in press)}
}

2018 (5)

Stefan Klikovits, Auélien Coet and Didier Buchs. ML4CREST: Machine Learning for CPS Models. In: 2nd International Workshop on Model Driven Engineering for the Internet-of-Things (MDE4IOT), CEUR Workshop Proceedings, vol. 2245, pp 515-520. 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 Link
Bibtex
@inproceedings{Klikovits:MDE4IOT:CREST,
  title={{ML4CREST: Machine Learning for CPS Models}},
  author={Stefan Klikovits and Aur\'{e}lien Coet and Didier Buchs},
  year = {2018},
  month = {01},
  pages = {515-520},
  url = {http://ceur-ws.org/Vol-2245/mde4iot_paper_4.pdf},
  volume = 2245,
  series = {CEUR Workshop Proceedings},
  booktitle = {2nd International Workshop on Model-Driven Engineering for the Internet-of-Things (MDE4IoT)}
}

Stefan Klikovits, Alban Linard and Didier Buchs. CREST - A DSL for Reactive Cyber-Physical Systems. In: Proceedings of 10th System Analysis and Modeling Conference (SAM), Lecture Notes in Computer Science, vol. 11150, pp 29-45. Springer, 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 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}},
  series={Lecture Notes in Computer Science},
  volume={11150},
  author = {Klikovits, Stefan and Linard, Alban and Buchs, Didier},
  editor = {Khendek, Ferhat and Gotzhein, Reinhard},
  year = {2018},
  month = {01},
  pages = {29-45},
  doi = {10.1007/978-3-030-01042-3_3}
}

Stefan Klikovits, Alban Linard, Dimitri Racordon and Didier Buchs. Petri Sport: A Sport for Petri Netters. In: Proceedings of International Workshop on Petri Nets and Software Engineering (PNSE), CEUR Workshop Proceedings, vol. 2138, 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 Link 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},
  editor = {Moldt, Daniel and Kindler, Ekkart and R{\"o}lke, Heiko},
  series = {CEUR Workshop Proceedings},
  volume = {2138},
  url = {http://ceur-ws.org/Vol-2138/paper2.pdf}
}

Didier Buchs, Stefan Klikovits, Alban Linard, Romain Mencattini and Dimitri Racordon. A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning. In: Proceedings of Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Lecture Notes in Computer Science book series, vol. 10877, pp 385-395. Springer, 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 = {Proceedings of Application and Theory of Petri Nets and Concurrency - 39th International Conference, {PETRI} {NETS} 2018},
  pages = {385--395},
  year = {2018},
  series = {Lecture Notes in Computer Science},
  volume = {10877},
  publisher = {Springer},
  doi = {10.1007/978-3-319-91268-4_21}
  url = {https://doi.org/10.1007/978-3-319-91268-4_21},
}

Stefan Klikovits, Alban Linard and Didier Buchs. CREST Formalization. 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)

Stefan Klikovits, Manuel Gonzalez-Berges and Didier Buchs. Towards Lanuguage Independent (Dynamic) Symbolic Execution. In: Proceedings of the 24th PhD Mini-Symposium, pp 50-53. Budapest University of Technology and Economics, Department of Measurement and Information Systems, 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},
}

Joachim Denil, Stefan Klikovits, Pieter J. Mosterman, Antonio Vallecillo and Hans Vangheluwe. The Experiment Model and Validity Frame in M&S. In: Proceedings of the Symposium on Theory of Modeling & Simulation, TMS/DEVS, pp 109-120. ACM, 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},
}

Stefan Klikovits, Joachim Denil, Alexandre Muzy and Rick Salay. Modeling Frames. In: 14th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa), CEUR Workshop Proceedings, vol. 2019, 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},
  volume = 2019,
  series = {CEUR Workshop Proceedings},
  pages = {315--320},
  year = {2017}
}

Stefan Klikovits, Alban Linard and Didier Buchs. CREST - A Continuous, REactive SysTems DSL. In: 5th International Workshop on the Globalization of Modeling Languages (GEMOC), CEUR Workshop Proceedings, vol. 2019, 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},
  url = {http://ceur-ws.org/Vol-2019/gemoc_2.pdf},
  volume = 2019,
  series = {CEUR Workshop Proceedings},
}

2016 (1)

Stefan Klikovits, David P. Y. Lawrence, Manuel Gonzalez-Berges and Didier Buchs. Automated Test Case Generation for the CTRL Programming Language Using Pex: Lessons Learned. In: Proceedings of 8th International Workshop on Software Engineering for Resilient Systems, Lecture Notes in Computer Science, vol. 9823, pp 117-132. Springer, 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 = {8th International Workshop on Software Engineering for Resilient Systems (SERENE)},
  pages = {117--132},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {9823},
  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)

Stefan Klikovits, David P. Y. Lawrence, Manuel Gonzalez-Berges and Didier Buchs. Considering Execution Environment Resilience: A White-Box Approach. In: Proceedings of 7th International Workshop on Software Engineering for Resilient Systems (SERENE), Lecture Notes in Computer Science, vol. 9274, pp 46-61. Springer, 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 = {7th International Workshop on Software Engineering for Resilient Systems (SERENE)},
  pages = {46--61},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {9274},
  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)

Paul C. Burkimsher, Manuel Gonzalez-Berges and Stefan Klikovits. Multi-platform SCADA GUI Regression Testing at CERN. In: Proceedings of the 13th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS). JACoW, 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}
}