1. Inleiding
Onder "formele methoden" worden talen en technieken verstaan, gebaseerd op de discrete wiskunde, die gebruikt kunnen worden bij de analyse, het ontwerp en de implementatie van (software) systemen. Herhaaldelijk worden er vraagtekens geplaatst bij de toepasbaarheid van formele methoden in de ontwikkeling van software-systemen in de industrie. De kwestie is echter niet of formele methoden in de praktijk bruikbaar zijn of niet. Ze worden namelijk al gebruikt, denk maar aan programmeertalen, generatoren, enz. Waar het om gaat is of formele methoden inzetbaar zijn in een vroeger stadium van het ontwikkelproces dan de uiteindelijkeimplementatieen wat voor zin dat heeft.
2. Gebruik van formele methoden in de praktijk.
Tijdens de IFIP conferentie van 1992 werd er geconstateerd dat er een groot verschil bestaat tussen datgene wat onderzoekers zeggen aan te bieden met formele methoden en datgene waar de industrie behoefte aan heeft.
Aanbod:
correcte software, exacte specificaties, hulp bij de constructie van complexe algoritmen en datastructuren, nieuwe methoden voor software-ontwikkeling, mensen die wiskunde kunnen toepassen in het ontwikkelproces, goed-gedeflnieerde systemen en garanties met betrekking tot de functionaliteit van systemen.
Vraag:
kortere ontwikkeltijd, evoluerende systemen, hulp bij de constructie van complexe systemen, incremented uitbreidingen van bestaande methoden, betere ontwerpers, systeemfamilies en garanties met betrekking tot prestaties, betrouwbaarheid, enz.
In een recent rapport over de toepassing van formele methoden in de industrie wordt geconcludeerd dat formele methoden weliswaar in een aantal aspecten de volwassenheid nog niet hebben bereikt, maar dat ze steeds meer in de industrie worden toegepast, serieus en met succes. Op veel plaatsen is men bezig met het introduceren van formele methoden. Bij Philips is voor het gebruik van formele methoden gekozen op grand van zaken als herbruikbaarheid, kortere ontwikkeltijd en het fout-vrij zijn van de software.
Een probleem dat optreedt bij de introductie van formele methoden in de praktijk is dat het gebruik veelal beperkt blijft tot een kleine kring van direct betrokkenen. Het opbouwen van kennis en kunde om met formele methoden te kunnen werken verloopt erg moeizaam binnen de organisaties die experimenteren met formele methoden.
3. Opleidingen
Zoals in het verleden het leren programmeren equivalent leek te zijn aan het leren van een programmeertaal, zo lijkt het leren gebruiken van formele methoden nu gelijk gesteld te worden aan het leren van een of andere formele specificatietaal. Maar zijn er gemeenschappelijke basisbegrippen achter de verschillende formele talen?
Als formele technieken ook in de praktijk van software-ontwikkeling een rol (gaan) spelen, moeten ontwikkelaars leren hoe ze met deze technieken kunnen omgaan en wat de achterliggende begrippen zijn. De technieken moeten niet alleen bruikbaar zijn voor wiskundigen en wiskundig georienteerde informatici op universiteiten, maar juist ook voor software ingenieurs in de praktijk.
Bij Philips zijn we in het begin van de tachtiger jaren gestart met de Cursus Software Ontwerp (CSO). In deze cursus wordt uitgebreid gebruik gemaakt van formele technieken om de constructeur bij zijn werkzaamheden te ondersteunen. Deze lijn werd doorgetrokken in de Cursus Software Engineering (CSE), waarin formeel werken en object-georienteerd werken zijn samengebracht. In 1992 is een cursus Formed Specificeren ontwikkeld, die nu aan revisie en uitbreiding toe is.
4. Slot
Om in de praktijk de acceptatie van formele methoden gemakkelijkerte maken, zal aangetoond moeten worden dat het inzetten van deze technieken en talen de produktiviteit en de kwaliteit in de softwareontwikkeling vergroten, zonder dat de kosten significant stijgen. Om dit te bereiken zal er aan ten minste drie punten aandacht moeten worden besteed:
- Zorg ervoor dat formele methoden ook in constructieve zin de software-ontwikkelaar van nut kunnen zijn. De methoden moeten de constructeur hints geven voor zijn ontwerp.
- Zorg ervoor dat de theorie "verteerbaar" wordt voor de software-ontwikkelaar. Een elektrotechnicus kan leren differentieren en integreren zonder dat hij/zij zich de achterliggende wiskundige theorie volledig eigen hoeft te maken.
- Begin nu met het opnemen van de basisprincipes van formele methoden in het onderwijsprogramma voor toekomstige software-constructeurs. Dat zal hen beter voorbereiden op de toekomst en tegelijkertijd de acceptatiegraad van formele methoden vergroten.