Resource page for experiments with formal specification validation in computer games.
A virtual environment, where validation and evaluation of railway controllers, developed by contemporary FM, can be realized in a form of gameplay. It consists of a modified version of the Open Rails train simulator (OR) and an application called TS2JavaConn (TS2JC), which provides communication between Open Rails and the controller.
Formal model of a cleaning robot safety-critical component, written in the B-language of B-Method. This model can be translated to C# or Java by the BKPI compiler.
BKPICompilerInstr.pdf.
Formal model of the cleaning robot safety-critical component, modified for use with the ProB 2.0 Java interface.
Game created in the Unity engine, which uses C# code, generated from the executable prototype formal specification by the BKPI compiler.
Game created in the jMonkeyEngine engine, which uses Java code, generated from the executable prototype
formal specification by the BKPI compiler.
The game logs execution times of the updateAndEvaluate method calls into a text file called logfile.txt.
Game created in the jMonkeyEngine engine, which animates the modified formal specification of the safety-critical component
via the ProB 2.0 Java interface, integrated into it.
The game logs execution times of the updateAndEvaluate method calls into a text file called logfile.txt.
This archive contains files with unusually long names, which some unpackers may fail to extract. We recommend to use WinRAR for the extraction.
JFireEmSim2 is an emergency simulation game, where the player is a fireman whose primary goal is to rescue a family from a house under fire. The game also includes the executable prototype of the robot controller, this time disguised as a secondary fireman. An interesting feature of the game is that non-playable characters are modelled as emotional BDI agents, simulated by Jadex with a JBdiEmo emotional engine.
To start JFireEmSim2, please unpack the archive and run MyGame.exe.