Welcome to the Model Treasure Trove!
Here, we collect and share models from various domains in many different formats. We start with the models that were given to us and we will sort them after we received a critical mass … 😉
Model 1: Turn Indicator (Daimler AG, University Bremen, Verified Systems)
The original website with the model can be found here. There, you will also find a paper about a benchmark model for testing that uses the presented model.
On our website, we mirror a pdf for an overview of the model, an xmi description, and a project file for Enterprise Architect 8.0.
Model 2: Pressure Sensor (Opel AG, Fraunhofer FIRST)
This model describes the behavior of a pressure sensor.
We provide the model in three different formats:
1) for Conformiq Test Designer (test generator is available here)
2) for UPPAAL (test generator is available here)
3) for Microsoft SpecExplorer (test generator is available here)
Here, you can find a paper describing the case study that includes a first comparison of the three different modeling approaches.
Model 3: Several Models in the Z-Notation (Universidad Nacional de Rosario)
This file contains several models in the Z-notation with a corresponding description in pdf (some of them are in Spanish). One corresponding test generator is Fastest. Some od the models describe banks, a launching vehicle, a lift, communication protocols, schedulers, sensors, voting systems, and more …
Model 4: Some models (for Java Set<T> interface and “QuiDonc”) from the University of Waikato
In this file you will find some models for the test generator modelJUnit. The java files can be directly executed with the test generator. For the QuiDonc example, there are also pdfs included for better visualization.
Model 5: Some EFSM models (CREST – University College London)
The (mostly academic) models contained in this file describe several artifacts in EFSM such as an ATM, a cashier, a cruise control, a fuel pump, a lift, or a vending machine. Thanks to the colleagues from the University College London. In this paper, the models are used for slicing of EFSMs.
Model 6: Abstracted model for a web service
The model contained in this graphML or sax file describes an abstracted and simplified Symbolic Transition System for a license management web application (WIBU SYSTEM’s CodeMeter License Central). The model was used to experiment with an extension of JTorX called LazyOTF, which synergetically integrates offline and on-the-fly MBT. The extension and experiments are described in this bachelor thesis and this upcoming dissertation. The sources are available in this git repository; you can check out the newest version of LazyOTF via git clone –branch LazyOTF/experimental https://vcs.utwente.nl/diffusion/JTORX/stsimulator.git. To build it via ant -f build_symtosim.xml, you need to follow the instructions in the README file.
Model 7: soon to come …