About / Advertise
När The Mathworks ger sig på formell verifiering av inbyggda system sker det med svensk hjälp. I det nya verktyget Simulink Design Verifier, avsett att automatisera testförfarandet, kommer tekniken för formell verifiering från Stockholmsbolaget Prover Technology.
The Mathworks, mest känt för beräknings- och simuleringsprogrammen Matlab och Simulink, utökar sin repertoar av verktyg for elektronikkonstruktion och inbyggda system. Tidigare har algoritmer och modeller kunnat skrivas i Simulink, varifrån mjukvara och hårdvara kunnat genereras i C och C++ respektive VHDL och Verilog. Nu lanseras ett verktyg for verifiering av den genererade hård- och mjukvaran kallat Simulink Design Verifier. Verktyget bygger på formella, matematiska metoder, och Mathworks har valt svenska Prover som leverantör av beräkningsmotorn.
- Vi har samarbetat tidigare, men det har är första gången som vi använder Prover i ett kommersiellt tillgängligt verktyg, säger Jim Tung på The Mathworks.
Tanken med det nya verktyget ar att hitta de buggar i en konstruktion som av en eller annan anledning inte fångas av simuleringsverktygen. Det utför dels så kallad ekvivalenskontroll som visar att den genererade hård- och mjukvaran beter sig exakt som modellen skriven i Simulink. Men - vilket är betydligt svårare - det kan också testa matematiskt om konstruktionen uppfyller en rad kriterier som användaren eller någon industristandard föreskriver. Användaren kan beskriva dessa egenskaper, så kallade properties eller assertions, och låta verktyget automatiskt generera tester för att se om konstruktionen uppfyller de önskade egenskaperna.
Beräkningsmotorn från Prover genererar testfallen. Den kan också alstra motexempel, som visar under vilka förhållanden det önskade beteendet inte uppstår. Prover har anpassat sitt gränssnitt for att passa verktygen från Mathworks.
