Mathworks voegt formele methodes toe aan Simulink

Reading time: 1 minute

Author:

The Mathworks heeft Simulink Design Verifier gelanceerd. De uitbreiding van het modelgebaseerde simulatieplatform genereert tests en geeft wiskundig bewijs over de eigenschappen van modellen uit Simulink en Stateflow. De toolbouwer baseerde het pakket op de Prover Plug-In-methode van het Zweedse Prover Technology.

Simulink Design Verifier is beschikbaar voor Linux en Windows.

The Mathworks besloot formele methodes in het ontwerpgereedschap op te nemen om ontwikkelaars van missiekritische toepassingen voldoende testdekking te geven. Het bedrijf verwacht dat vooral embedded-software-engineers de nieuwe feature zullen gebruiken, maar ook andere hardware- en softwareontwerpers kunnen ervan profiteren. Hoewel er in theorie geen technische hindernissen zijn, is de nieuwe tool bedoeld voor een systeem met een ’redelijk aantal blokken‘ en geen duizenden.

’Formele methodes geven ontwerpers de mogelijkheid om te testen en fouten te vinden die heel lastig te vinden zijn met simulatie alleen‘, zegt Paul Bernard, marketingdirecteur Designautomatisering bij The Mathworks. ’Je kunt wel uitentreuren simuleren om alle bugs te vinden, maar formele methodes leveren simpelweg een beter resultaat.‘

Om tests te genereren met Design Verifier moeten gebruikers een model aanleveren en de dekking en testdoelen specificeren. Behalve testvectoren geeft de tool een testharnas, inclusief inputwaarden en verwachte uitkomsten. Ook informeert het gereedschap over eigenschappen waar niet aan is voldaan.