Bosch und Daimler zeigen fahrerloses Parken im realen Verkehr: Weltpremiere im Parkhaus des Mercedes-Benz Museums

‘Onzekere’ software toch voorspelbaar maken

Gepubliceerd op 22-05-2018 om 12:49

Fahrerloses Parken im realen Verkehr: Weltpremiere im Parkhaus des Mercedes-Benz Museums. Per Smartphone-Befehl fahren Autos fahrerlos in einen zugewiesenen Stellplatz, ohne dass der Fahrer das Manöver noch überwachen muss. Möglich wird das fahrerlose Parken mithilfe einer intelligenten Parkhaus-Infrastruktur von Bosch im Zusammenspiel mit der Fahrzeugtechnik von Mercedes-Benz. Driverless parking in real-life traffic: World premiere in the multi-storey car park of the Mercedes-Benz Museum. Cars proceed without a driver to an assigned parking space in response to a command issued by smartphone, without any need for the driver to supervise the manoeuvre. Driverless parking is made possible by an intelligent multi-storey car park infrastructure from Bosch in conjunction with the vehicle technology from Mercedes-Benz.

Software die rekening houdt met allerlei risico’s en onzekerheden wordt steeds belangrijker in de wereld van kunstmatige intelligentie, waartoe ook zelfrijdende auto’s behoren. Professor Joost-Pieter Katoen van de Universiteit Twente gaat onderzoeken hoe je kunt nagaan of die software, met al die onzekerheid, toch goed werkt. Aan het onderzoek is een beurs van 2,5 miljoen euro toegekend.

Katoen is verbonden aan zowel de RWTH in Aken als de Universiteit Twente. Zijn onderzoek zal zich richten op probabilistische computerprogramma’s: software die te maken krijgt met heel veel onzekere en ‘real world’-data. De zelfrijdende auto baseert zijn rijgedrag op zulke software en de autonome robot kan straks ook niet zonder. Maar hoe kun je, bij al die onzekerheid, verifiëren of de software ook goed werkt? Daar zal het onderzoek van Katoen zich op richten.

Oneindig veel toestanden

De instrumenten die programmeurs normaal gesproken voor die verificatie kunnen gebruiken, volstaan niet bij probabilistische computerprogramma’s. Dat ligt aan het omgaan met onzekerheid. Gebruikelijke software heeft al oneindig veel toestanden waarin het programma kan verkeren. Het doorrekenen hiervan is vrijwel onmogelijk.

Formele programma verificatie is een een techniek die een programmeur helpt bij het vaststellen van de correcte werking. Probabilistische programma’s zijn echter nog lastiger te doorgronden, omdat ze omgaan met onzekere data en real-world observaties. Het is eigenlijk niet mogelijk om een conclusie trekken over de correcte werking als dat is gebaseerd op statistische gegevens over deze onzekere data.

Drastisch andere benadering

Simulatietechnieken schieten te kort als het moeilijk wordt. Onderzoekers weten in zo’n geval niet hoe lang ze door moeten gaan met simuleren en de situaties geven geen harde garantie, aldus Katoen. Volgens hem is formele verificatie ook hier dé manier om deze tekortkomingen het hoofd te bieden. Dat is een drastisch andere benadering, maar wel hard nodig omdat probabilistische software steeds vaker bepalend gaat worden voor bijvoorbeeld onze dagelijkse veiligheid. De zelfrijdende auto baseert er straks zijn beslissingen op.

Katoen wil de techniek van ‘programmaverificatie’ ook geschikt maken voor probabilistische software: deze techniek rekent aan software nog vóórdat het programma wordt uitgevoerd op een computer. Op die manier komen fouten en onverwacht gedrag aan het licht. Probabilistisch programmeren gaat nadrukkelijk niet over software die zich ‘random’ gedraagt, aldus Katoen: “Formele verificatie gaat het voorspelbaar maken.”