A Communicating Transaction Process (CTP) is a computational model based on Message Sequence Charts (MSC) to describe a network of communicating components. Intensive study has been dedicated to the application and analysis of CTP models, but little work has reported formal methods of designing them. This paper attempts to bridge the gap with Supervisory Control Theory (SCT), so that the CTP models meet all predefined constraints and possess the required system properties. SCT is implemented by XPTCT software and the control logic obtained can be easily translated into propositional formulas for guarded MSCs.
展开▼
