Specification of Systems Theory in Search for Prac

HILDESHEIMERINFORMATIK-BERICHTEUNIVERSITÄTHILDESHEIMPostfach10136331113HildesheimInstitutfürInformatikDieserBerichtistherausgegebenvomE.Brinksma,J.Parrow,A.Rensink(organisers)St.Heymer(editor)SpecificationofSystems:TheoryinSearchforPracticeSummaryofaWorkshop24/94(September1994)ISSN0941-3014(thispageintentionallyleftblank)SpecicationofSystems:TheoryinSearchforPracticeSummaryofaWorkshopHildesheim,Germany,7{9March1994EdBrinksma,JoachimParrow,ArendRensink(organisers)StefanHeymer(editor)iiContentsForeword:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::1Workshopprogramme:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::3OveFaergemand,EURESCOM:TheUseofFormalDescriptionTechniquesinStandardisationWork:::::::::::::::::5JanFrisoGroote,UniversityofUtrecht:Vericationandproofcheckingoflargerprotocols:::::::::::::::::::::::::::::::::::6EdBrinksma,UniversityofTwente:WhatistheMethodinFormalMethods?:::::::::::::::::::::::::::::::::::::::::::7RobertoGorrieri,UniversityofBologna:CanFormalMethodsbeUsefulforSecurity?:::::::::::::::::::::::::::::::::::::::8JanPeleska,DeutscheSystemtechnik:EcientHigh-QualityEvaluationofITSecurityProducts:::::::::::::::::::::::::::9WilJanssen,UniversityofTwente:PartialOrderBasedDesignofDistributedSystems::::::::::::::::::::::::::::::::10RonKoymans,PhilipsResearchLaboratories:SoftwareEngineeringinIndustry:IssuesandChallenges:::::::::::::::::::::::::::13MartenSaund,Logikkonsult:IndustrialApplicationofFormalVerication:::::::::::::::::::::::::::::::::::::::14OveAkerlund,SAABMilitaryAircraft:UsingNPCircuitforAnalysisofSystemSafetyandReliability:::::::::::::::::::::16iiiRomLangerak,UniversityofTwente:FormalMethodsintheDesignTrajectory::::::::::::::::::::::::::::::::::::::::::17UrsulaGoltz,UniversityofHildesheim:RenementandAbstractionfordevelopingReactiveSystems:::::::::::::::::::::::18StevenKlusener,CWI:VericationofanAudioprotocol::::::::::::::::::::::::::::::::::::::::::::::::::19HansHook,SICSAboutIntegrationofFormalDescriptionTechniquesandSystemsDevelopmentProcesses:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::20Listofparticipants:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::21ivForewordSpecicationanddesignofdistributedcomputersystemsisacomplexanderror-proneaair,andlargeeortsarethereforemadeondevelopmentofappropriatedesignmethods.Butthereisagapbetweentheoryandpractice:thebenetsoftheoreticalsupportarenotbeingrealizedinpractice,andconverselythetheoreticdevelopmentsdonotreceiveanyfeedbackornewimpulsesfrompracticalapplication.TheinternationalworkshoponSpecicationofSystemsattheUniversityofHildesheim,7{9March1994,attractedparticipantsfromacademiaandindustryinasmallscaleat-tempttobridgethisgap.Thepurposewastodenelinesofresearchthatseempromisingforfutureapplication,tosingleoutcasestudiesofmanageablesizefortheoreticians,andtostudyissuesofexpressivity.Thepresentationsoftheparticipantsfromindustrycon-stitutedthebackboneoftheworkshop.Theywerefollowedbybriefdiscussionsessions.Theacademicparticipantsgaveshortpresentationsoftheirownwork,withanemphasisonapplicability.Inthisreportwecollectthescheduleoftheworkshop,abstractsofthetalksandthelistofparticipants.Wethankallparticipantsforcontributingtoaninterestingworkshop,andthelocalsupport,consistingofVeraDoeringandStefanHeymer(bothofwhominadditionaidedincompilingthisreport)andThomasHaakeformakingitpossible.Finally,wegratefullyacknowledgenancialsupportgrantedbytheTechnologyTransferoceoftheUniversityofHildesheim.EdBrinksmaJoachimParrowArendRensink(localorganiser)12WorkshopProgrammeMonday,March7th13.00Registrationandsnacks13.45Wordofwelcome14.00OveFaergemand,EURESCOMTheUseofFormalDescriptionTechniquesinStandardisationWork15.00Discussion15.15JanFrisoGroote,UniversityofUtrechtVericationandproofcheckingoflargerprotocols15.45Teaandcoeebreak16.15EdBrinksma,UniversityofTwenteWhatistheMethodinFormalMethods?17.15Discussion17.30RobertoGorrieri,UniversityofBolognaCanFormalMethodsbeUsefulforSecurity?Tuesday,March8th9.00JanPeleska,DeutscheSystemtechnikEcientHigh-QualityEvaluationofITSecurityProducts10.00Discussion10.15WilJanssen,UniversityofTwentePartialOrderBasedDesignofDistributedSystems10.45Coeeandteabreak311.15RonKoymans,PhilipsResearchLaboratoriesSoftwareEngineeringinIndustry:IssuesandChallenges12.15Discussion12.30Lunch14.00JanPeleska,DeutscheSystemtechnikFormalSpecicationMethodsfortheControlofDecentralisedSemaphores14.30MartenSaund,LogikkonsultIndustrialApplicationofFormalVerication15.30Discussion15.45Teaandcoeebreak16.15OveAkerlund,SAABMilitaryAircraftUsingNPCircuitforAnalysisofSystemSafetyandReliability17.15Discussionsession:Whitherformalmethods?Wednesday,March9th9.15RomLangerak,UniversityofTwenteFormalMethodsintheDesignTrajectory9.45UrsulaGoltz,UniversityofHildesheimRenementandAbstractionfordevelopingReactiveSystems10.15StevenKlusener,CWIVericationofanAudioprotocol10.45Coeeandteabreak11.15HansHook,SICSAboutIntegrationofFormalDescriptionTechniquesandSystemsDevelopmentPr