Abstrakt. Webbtjänster är distribuerade programvarukomponenter, som frikopplas från varandra med hjälp av gränssnitt med specificerade funktionella beteenden. Sådana beteendespecifikationer är dock otillräckliga för att visa överensstämmelse med vissa tidsbundna icke-funktionella policyer. Ett exempel visar att en patients hälsorelaterade fråga som skickas till en hälso- och sjukvårdstjänst endast besvaras av en läkare (och inte av en sekreterare). Att visa överensstämmelse med sådana riktlinjer är viktigt för att tillfredställa statliga integritetsregler. Det är ofta nödvändigt att avslöja de interna delarna av genomförandet av webbtjänsten för att visa sådan överensstämmelse, vilket kan äventyra modulariteten. I detta arbete tillhandahåller vi en språkdesign som möjliggör sådana demonstrationer, samtidigt som de flesta av tjänstens källkod döljerskod. Den viktigaste idén är att använda gråbox specifikationer för att göra det möjligt för tjänsteleverantörer att selektivt dölja och avslöja delar av deras genomförande. Det övergripande problemet med att visa överensstämmelse reduceras sedan till två delproblem: om de önskade egenskaperna är uppfyllda av tjänstens gråboxspecifikation och om denna gråboxspecifikation är nöjd med tjänstens genomförande. Vi specificerar policyer med hjälp av LTL och löser det första problemet genom modellkontroll. Vi löser det andra problemet genom förfiningsteknik.
Rajan m.fl. REF använder gråbox specifikation för att resonera om webbtjänstpolicyer.
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services ⋆
{'venue': 'ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}