Team "Semantics, Modeling & Verification"
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
LICENSE Initial commit Jun 14, 2017

Developing complex and reliable software systems requires rigorous methods for modelling, designing and verifying them. The SMV group is involved in designing dedicated formalisms that are semantically well described in order to make analysis of system properties possible, to automatically produce code and to select pertinent test cases. A coherent set of tools has been developed in order to apply our methods to software-intensive systems.

Bachelor projects

The SMV group is currently creating an automated plant growing system connected to the Internet of Things (IoT). The system consists of single-board computers (Raspberry Pi), various sensors (light, distance, temperature, humidity) and actuators (water pumps). Currently various different software libraries are necessary to interact with these peripheral devices locally, while remote access to the sensor readings is not possible.

  • [IoT data visualisation]({{ site.url }}/team-smv/assets/bachelor-projects-1.pdf)

    The goal of this project is to connect the systems to the IoT. This will be performed by introducing a homogeneous API locally on the Raspberry Pi. This API should be accessible programmatically from other systems (e.g. through a REST interface). Further, a web user interface should be created to stream data to the internet and provide remote monitoring capabilities to any users. For this part an evaluation of existing IoT platforms (,,, etc.) should be performed and evaluated against an own, application-specific development using HTML, CSS3 & JavaScript libraries. The final outcome will be a monitoring and control software that is versatile and can be accessed platform independently.

  • [IoT Scheduling and Planning]({{ site.url }}/team-smv/assets/bachelor-projects-2.pdf)

    The goal of this project is to create a scheduling and planning API for the IoT system. This will be implemented by introducing an API locally on the Raspberry Pi that allows users to define a schedule for sensor readings and actuator actions. The controller should then follow the plan and perform the actions as specified. The definition of the plan should be possible both programmatically via a REST API (e.g. using JSON/XML/...) or with a web user interface. This user interface should provide an appealing and easily comprehensible means to view and edit the current execution plan. This can be implemented by using one of the many already existing JavaScript libraries. The final outcome will be a monitoring and scheduling controller that is versatile and can be accessed platform independently.

The SMV group is currently developing CREST, a graphical modeling language for the design of home automation, automatic plant growing and similar systems. While the first version of the language is being implemented in Python, a graphical editor is necessary for user friendly interaction.

  • [Web based modeling editor]({{ site.url }}/team-smv/assets/bachelor-projects-3.pdf)

    The goal is to create a versatile and extensible prototype web editor for the representation of CREST diagrams. The development should be based on existing plotting and layout libraries (D3.js, Cytoscape.js, ELK.js). The features to develop include creation, modification and layouting of component-and-connector views, collapsing/uncollapsing of nested nodes and redrawing of information. Depending on the student’s interests, it is possible to pursue three different specialisations of this project:

    • layouting and visualisation of CREST diagrams: research into the optimal position of diagram elements to facilitate reading and information flow
    • GUI design: evaluate different interaction opportunities within browser based graphical editors and facilitate object manipulation
    • backend communication: communication, synchronization and consistency between the web front-end with the Python-based backend

Job Offers

There is currently no job.

Domains of Activity

  • Development of techniques for distributed object-oriented and reconfigurable system modelling
  • Test selection techniques
  • Model validation
  • Software prototyping
  • Model engineering (MDA,UML, model transformation)

Domains of Application

  • Embedded systems
  • Ubiquitous systems
  • Enterprise web-based systems
  • Safety engineering : System and Human Risk Analysis (in collaboration with the Institute of Occupational Health Sciences, Lausanne)


| :--- | :---: | :--- | :--- | | Didier Buchs | | Professor | | | Stefan Klikovits | | Ph.D. Student | | | Alban Linard | | Post-doc | | | Dimitri Racordon | | Ph.D. Student | | | Steve Hostettler | | Senior Lecturer | |

Former Members

  • David Lawrence
  • Edmundo López Bóbeda
  • Alexis Marechal
  • Maximilien Colange
  • Mihai-Lica Pura
  • Steve Hostettler
  • Qin Zhang
  • Matteo Risoldi
  • Ang Chen
  • Levi Lúcio
  • Andrey Berlizev - Andy sadly left us in April 2009
  • Luis Pedro
  • Paula Mangas
  • David Hurzeler
  • Adel Besrour
  • Shane Sendall
  • Stanislav Chachkov
  • Jacques Flumet
  • Julie Vachon
  • Cécile Péraire
  • Giovanna Di Marzo
  • Stéphane Barbey
  • Pascal Racloz
  • Jarle Hulaas
  • Nicolas Guelfi
  • Sandro Costa
  • Mathieu Buffo
  • Olivier Biberstein



Our mail address is:

Semantics, Modeling & Verification Maboratory
University of Geneva
Battelle Bat. A
Route de Drize 7
CH-1227 Carouge


Our team uses the following tools:

  • BitBucket for private data, such as paper sources, talk sources, or course sources
  • GitHub for our homepage, courses and software
  • ResearchGate for our projects and articles
  • Overleaf to write papers, that should be put after completion in BitBucket

A new member of the Semantics, Modeling and Verification team should create accounts in all the services above, and request to become a member of our team in BitBucket and GitHub.