Action Refinement for Real-Time Concurrent Processes with Urgency

(整期优先)网络出版时间:2005-04-14
/ 1
Actionrefinementforreal-timeconcurrentprocesseswithurgentinteractionsisstudied,whereapartial-ordersetting,i.e.,timedbundleeventstructures,isusedasthesystemmodelandareal-timeLOTOS-likeprocessalgebraisusedasthespecificationlanguage.Itisshownthattheproposedrefinementapproacheshavethecommonlyexpectedproperties:(1)thebehaviouroftherefinedprocesscanbeinferredcompositionallyfromthebehaviouroftheoriginalprocessandfromthebehaviouroftheprocessessubstitutedforactions;(2)thetimedextensionsofpomset(partiallyorderedmultiset)traceequivalenceandhistorypreservingbisimulationequivalencearebothcongruencesundertherefinement;(3)thesyntacticandsemanticrefinementscoincideuptotheaforementionedequivalencerelationswithrespecttoacpo-baseddenotationalsemantics.