Implementatie van de Life cycle checker

In de begintijden van de computer was het de gewoonste zaak van de wereld dat een programmeur een miniscuul stukje code ging optimaliseren, maar met hededaagse commerciele ontwikkelingen gaat dat niet meer, enerzijds omdat de applicaties zo groot zijn dat altijd het overzicht moet worden gehouden, anderzijds omdat de ontwikkelingen razendsnel gaan en er weinig tijd is voor `kleinigheden' als efficientie.

In een poging om in te springen op deze behoeften van software-ontwikkelaars wordt steeds meer geprobeerd software-ontwikkeling op een hoger plan te brengen. We zien dit aan GUI builders die veel standaardwerk voor ons doen, aan CASE-tools die saaie stukken code voor ons genereren en aan hoog-nivo scripting talen als Python en Perl. Twee algemene nodigheden om software-ontwikkeling te verbeteren zijn mijns inziens het behoud van overzicht over een complex geheel en het zo vroeg mogelijk betrapt worden op fouten.

Mijn Life cycles zijn een manier om (de proces-aspecten van) een applicatie op hoog niveau te kunnen modelleren. Deze modellen hebben een krachtige maar eenvoudige semantiek, wat ze prettig maakt als modelleringstool, maar zonder de mogelijkheid te verliezen allerhande analyses er op los te laten. Deze analyses behelzen eigenschappen die de ontwerper verwacht te kunnen aantonen uit de modellen, maar ook eigenschappen die ten grondslag liggen aan Life cycles zelf (bijvoorbeeld referential integrity).

Voor het uitvoeren van de analyse van deze eigenschappen zijn wij bezig een theorie af te ronden, die het midden houdt tussen model checking en theoremabewijzen. Naarmate deze theorie slimmer wordt geimplementeerd is het mogelijk meer van de efficiente model checking technieken te gebruiken, en meer implementatieproblematiek van theoremabewijzen te vermijden. Dit kan er zowel voor zorgen dat de feedback uit de analyser beter begrijpelijk wordt voor de ontwerper, alsook dat de analyse zo vaak mogelijk gelijk heeft als hij een ontwerp afkeurt (hij heeft natuurlijk altijd gelijk als hij iets goedkeurt).

Voor deze klus zoeken we binnenkort mogelijk een werknemer die bereid is hier een aantal dagen per week aan te besteden, tegen de gebruikelijke vergoedingen. Deze opdracht wordt vermoedelijk gecombineerd met de automatische generatie van doorvlochten C code. Voor informatie kun je langskomen, bellen of mailen met Rick van Rein.