Groove
Groove is een afkorting van GRaphs for Object-Oriented VErification. Groove is een project rond het gebruik van eenvoudige grafieken voor het modelleren van de ontwerptijd, compilatie en looptijd structuur van objectgeoriënteerde systemen en grafiek transformaties als basis voor model transformatie en operationele semantiek. Dit betekent een formele basis voor model transformatie en dynamische semantiek en de mogelijkheid om model transformatie en dynamische semantiek te verifiëren via een (automatische) analyse van de resulterende grafiek transformatiesystemen, bijvoorbeeld met behulp van modelcontrole.

De Groove gereedschapset bevat een editor voor het maken van grafiek productie regels, een simulator voor het visueel berekenen van de grafiek transformaties veroorzaakt door een reeks van grafiek productie regels, een generator voor het automatisch verkennen van toestand ruimtes, een model checker dat CTL en LTL formules ondersteunt en een imaging tool voor het omzetten van grafieken naar afbeeldingen.

Een lijst van functies:
Hier is een korte lijst van ondersteunde functies door Groove. Voor meer informatie raadpleeg a.u.b. de meegeleverde handleiding of quick reference poster, of de demo's op de website.
  • Visueel bewerken en simulatie van grafieken en grafiek transformatie regels
  • Globale regel prioriteiten of controleprogramma
  • Toestandsruimte verkenning door gebruik te maken van aangepaste verkennings strategieën
  • Model checking generated transition systems op CTL en LTL formules
  • Reguliere expressie matching en label wildcards in transformatie regels
  • Primitieve data types (int, string, bool and real) met bijbehorende acties
  • Geneste (dat wil zeggen, gekwantificeerd) regels
  • Typing en overerving door middel van knooppunt types
  • Proloog opvragen van grafieken en toestandsruimte

Systeemvereisten
  • Minimaal Java versie 1.6ga5

Groove op een eComStation machine met Open JDK


Installeren van Groove
Download groove-4_8_7-bin.zip. Maak een map(directory) "Groove". Open het zip bestand en ga in de submap(subdirectory) "groove-4_8_7" staan. Kopieer alle bestanden en submappen(subdirectories) naar de nieuw aangemaakte map(directory) "Groove". De volgende versie (groove-4_9_0) heeft Java 1.7 nodig en de nieuwste versie (groove-5_5_6) Java 1.8.
Je moet ook de voorbeelden grammatika downloaden groove-4_8_7-samples.zip. Open het zip bestand en ga in de submap(subdirectory) "groove-4_8_7" staan. Kopieer de submap(subdirectory) "samples" naar de nieuw aangemaakte map(directory) "Groove". Dat is alles! Meer voorbeelden zijn te vinden in de svn repository, maar hier moet je zoeken naar de juiste versie op datum in plaats van versienummer. Ik heb het voorbeeld "ferryman.gps" aan het bestand "groove-ecs.zip" toegevoegd omdat het veerman probleem gebruikt wordt in de "Introduction to Groove" en dit probleem niet meegeleverd wordt in de voorbeeld bestanden. Om dit probleem te installeren moet je het zipbestand openen en gaan staan in de submap(subdirectory) "samples". Kopieer de submap(subdirectory) "ferryman.gps" naar de submap(subdirectory) "Groove\samples".

Het simulator.cmd bestand
Groove werkt met Open JDK in OS/2-eCS. Het is een gereedschap dat bestaat uit een aantal programma's, lees a.u.b. de bijgevoegde handleiding. Er zijn ook enkele demo's en de "Introduction to Groove" gebruikt de simulator. Daarom heb ik een "simulator.cmd" bestand gemaakt met de volgende inhoud; 
@echo off
set path=[station: java]\JAVA160ga5\bin
set BEGINLIBPATH=[station: java]\JAVA160ga5\bin
set CLASSPATH=
[station: groove]
cd [station: groove]\Groove
java -Duser.home=[station: groove]\Groove -jar .\bin\Simulator.jar 2>groove-bugs.txt
Ik gebruik 2 aparte mappen(directories), een voor Java en een voor Groove met de door het programma aangemaakte bestanden. De in het cmd bestand gebruikte verwijzingen;

  • [station: java] = station met Java
  • [station: groove] = station met Groove

moeten dus vervangen worden door echte schijfletters. Bewaar het bestand en geef het de naam "simulator.cmd" of gebruik het bestand uit onderstaande distributie. Dit bestand wordt gekopieerd naar de "Groove" map(directory). Verder kunnen paden anders zijn, pas dit naar behoefte aan.
Maak een nieuw programma object. Geef pad en de bestandsnaam op: "[station: groove]\Groove\simulator.cmd". In het tabblad Sessie de selectievakjes "OS/2 venster", "Starten als pictogram" en "Venster sluiten bij einde programma" aanvinken. In het tabblad Algemeen kan bij naam "Groove" worden opgegeven. In onderstaande distributie zit een geschikt OS/2 icoontje.

Parameters / opties verklaard
  • Met de opgave "-Duser.home=[station: groove]\Groove" wordt ervoor gezorgd dat Groove alle benodigde bestanden in de eigen directory opslaat inplaats van in de Home directory.
  • De toevoeging "2>groove-bugs.txt" zorgt ervoor dat foutmeldingen in het bestand "groove-bugs.txt" worden bewaard. De 2 in "2>" is geen typefout!

Download
In het bestand zit bovenstaand cmd bestand (alle schijfletters staan op C:) en OS/2 Groove icoontjes. Inbegrepen is ook het voorbeeld gebruikt in de demo "Introduction to Groove". Er zijn meer programma's, indien nodig kun je hiervoor een aangepast opdrachtbestand gebruiken: groove-ecs.zip.

revisie 11 september 2016