ENGINEERINGNET.BE - Model checking is een van de meest rigoureuze technieken om software te checken. Er wordt gekeken naar alle mogelijke acties die een softwaresysteem kan doen, en alle 'toestanden' waar het zich in kan bevinden, om te zien of alles werkt zoals het moet.

De uitdaging is dat software vaak uit meerdere delen bestaat die naast elkaar hun werk doen. Daardoor kan het aantal toestanden om te checken explosief toenemen, wat model checking duur en soms zelfs ondoenbaar maakt.

Neele heeft nieuwe manieren verkend om dit probleem aan te pakken en ervoor te zorgen dat minder toestanden gecheckt hoeven te worden.

De methodes van Neele hebben een ding gemeen: ze houden per toestand de vereisten in de gaten. Deze extra informatie maakt het makkelijker om te bekijken welke toestanden niet gecheckt hoeven te worden.

Om tegelijkertijd naar het systeemgedrag en de vereisten te kunnen krijgen, moest Neele eerst een nieuwe, gestructureerde manier ontwikkelen om de combinatie van vereisten en gedrag te laten zien.

De eerste techniek vermindert het aantal toestanden om te checken door gelijksoortige toestanden bij elkaar te groeperen. Dit maakt het zelfs mogelijk om met een oneindig aantal toestanden te werken.

De tweede methode controleert of parallelle onderdelen soms onafhankelijk van elkaar werken. Als dat zo is, dan is het niet nodig om alle mogelijke toestanden te bestuderen. De laatste techniek controleert of bepaalde informatie relevant is en verwijdert die als dat niet zo is.

In de toekomst kunnen deze ideeën ervoor zorgen dat kritieke software sneller en goedkoper ontwikkeld kan worden. Op dit moment is er veel expertise nodig om Neeles ideeën, en model checking in het algemeen, te kunnen toepassen.

Om meer algemeen gebruik mogelijk te maken, moet er een volledig geautomatiseerd systeem gebouwd worden dat bepaalt welke methode het beste past bij specifieke toepassingen. << (Lydia Heida) (foto: rawpixel - 123RF)

Mis ook dit niet... Vlaanderen op tweede plek in Europees innovatieonderzoek Het laatste Europese innovatieonderzoek toont dat de innovatiegraad in Vlaanderen voor 2016-2018 rond de 70% ligt. Daarmee behoort Vlaanderen tot de Europese top, enkel Estland doet beter. Kunstmatige intelligentie: nieuwer is niet altijd beter - opinie Wat triggert kopersverdriet? Sommigen voelen het al na enkele seconden na een impulsaankoop. We maakten het allemaal wel eens mee, maar dat maakt het er niet minder pijnlijk op. Automatiseer met één voordelige kickstart Heeft u weinig of geen ervaring? De SIMATIC S7-1200-starterkit is makkelijk, snel, compact en kostenefficiënt en bevat alle benodigde componenten om succesvol te automatiseren. Opheffing moratorium leidt voorlopig niet tot meer faillissementen Tijdens de maand februari 2021 gingen er 540 bedrijven failliet, een daling met 43% tegenover 2020. Januari en februari samengeteld toont 999 faillissementsuitspraken of 49,4% minder. Project: software robots om administratieve routinetaken over te nemen Het gebruik van databots, een toepassing van Robotic Process Automation (RPA), heeft het potentieel om automatisering snel en goedkoop toe te passen. VIL wil dit onderzoeken. Start bouw allereerste Vlaamse opleidingscentrum voor farma en biotech ViTalent en POM Antwerpen hebben het startschot gegeven voor bouw van allereerste opleidingscentrum voor farma en biotech in Vlaanderen. Vanaf begin 2022 worden opleidingen op maat aangebode Watson-Marlow en Bredel vanaf nu onder één dak De Watson-Marlow Fluid Technology Group (WMFTG) verzorgt vanaf nu de directe verkoop, de ondersteuning en de service van de industriële Bredel slangenpompen. ‘The 7 Transformations Experience’ - column Hoe groot of klein ze ook is, en ongeacht de menselijke en financiële middelen waarover ze beschikt, uw onderneming is in staat om te evolueren. 'The 7 Transformations Experience' helpt. STEREO III-project MUZUBI: vulkaanrisico bepalen met interferometrie Het Centre Spatial de Liège heeft een nieuwe techniek ontwikkeld die absolute hoogte- en verplaatsingsmetingen kan uitvoeren, voor het bepalen van de risico's van vulkaanuitbarstingen. Wie gaat er mee naar Mars? - artikel De mensheid blijft op aarde tot die wegkwijnt of ze springt naar andere planeten, zo stelt Elon Musk, die SpaceX oprichtte om ruimteschepen te ontwikkelen die ons naar Mars zullen brengen. FIBEr-labo erkend als ‘KU Leuven Kernfaciliteit’ In het FIBEr-labo van KU Leuven wordt het effect onderzocht van mechanische belasting op gezond, ziek of hersteld lichaamsweefsel. Dit labo is nu erkend als ‘KU Leuven Kernfaciliteit’.

Flexim lanceert nieuwe ultrasone flowmeters voor stoom Met de FLUXUS ST en FLUXUS ST-HT serie kan verzadigde stoom gemeten worden zonder inbreng van sensors in de leiding of het openen van de leiding. Ook het verjongen van de leidingdiameters is niet langer nodig om de stoomsnelheid te verhogen voor het toe te passen meetprincipe, want de flow kan al gemeten worden vanaf 1cm/s. Micro-Fulfillment na de pandemie Een micro-fulfilment distributiestrategie kan bestaande/gesloten stedelijke winkelruimtes herbestemmen als hybride retail-/distributie­knoop­punten. Deze hubs bieden naast een snellere levering van bestellingen ook de mogelijkheid om consumenten te laten kiezen tussen thuislevering of afhalen. Deze trend is versneld door de Covid-19-crisis. Topjobs op Engineeringnet Onze Belgische jobboard 'Engineeringnet TopJobs' onderscheidt zich door specialisatie. We bieden u als recruiter een platform met uitsluitend technische bezoekers aan (knelpuntberoepen!). Dat is een doelgroep die via andere kanalen zéér moeilijk bereikbaar is.