{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T08:46:47Z","timestamp":1748335607361},"reference-count":0,"publisher":"World Scientific Pub Co Pte Lt","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[1996,6]]},"abstract":"<jats:p> Formal methods such as CSP (Communicating Sequential Processes) are widely used for reasoning about concurrency, communication, safety, and liveness issues. Some of these models have been extended to permit reasoning about real-time constraints. Yet, the research in formal specification and verification of complex systems has often ignored the specification of stochastic properties of the system under study. We are developing methods and tools to permit stochastic analyses of CSP-based specifications. Our basic objective is to evaluate candidate design specifications by converting formal systems descriptions into the information needed for analysis. In doing so, we translate a CSP-based specification into a Petri net which is analyzed to predict system behavior in terms of reliability and performability as a function of observable parameters (e.g., topology, fault-tolerance, deadlines, communications, and failure categories). This process can give insight into further refinements of the original specification (i.e., identify potential failure processes and recovery actions). Relating the parameters needed for performability analysis to user level specifications is essential for realizing systems that meet user needs in terms of cost, functionality, and other nonfunctional requirements. <\/jats:p><jats:p> An example translation is given (in addition, some general examples of CSP \u2192 Petri net translations can be viewed in Appendix A). Based on this translation, we report both the discrete and continuous time Markovian analysis which provides reliability predictions for the candidate specification. The term \u201cCSP-based\u201d is used here to distinguish between the notation of Hoare\u2019s original CSP and our textual representations which are similar to occum. Our CSP-based grammar does not restrict consideration of the properties of CSP (traces, refusal sets, livelock, etc.), but we are not considering those properties. We are only interested that the structural properties are preserved. We define performability as a measure of the system\u2019s ability in meeting deadlines, in the presence of failures and variance in task execution times. <\/jats:p>","DOI":"10.1142\/s0218194096000119","type":"journal-article","created":{"date-parts":[[2004,9,6]],"date-time":"2004-09-06T07:50:09Z","timestamp":1094457009000},"page":"229-248","source":"Crossref","is-referenced-by-count":2,"title":["SPECIFICATION AND ANALYSIS OF REAL-TIME SYSTEMS USING CSP AND PETRI NETS"],"prefix":"10.1142","volume":"06","author":[{"given":"KRISHNA M.","family":"KAVI","sequence":"first","affiliation":[{"name":"The University of Texas at Arlington, 416 Yates Ave., PO Box 19015, Arlington, Texas 76019, USA"}]},{"given":"FREDERICK T.","family":"SHELDON","sequence":"additional","affiliation":[{"name":"The University of Texas at Arlington, 416 Yates Ave., PO Box 19015, Arlington, Texas 76019, USA"}]},{"given":"SHERMAN","family":"REED","sequence":"additional","affiliation":[{"name":"The University of Texas at Arlington, 416 Yates Ave., PO Box 19015, Arlington, Texas 76019, USA"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194096000119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T21:37:49Z","timestamp":1565127469000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194096000119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,6]]},"references-count":0,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[1996,6]]}},"alternative-id":["10.1142\/S0218194096000119"],"URL":"https:\/\/doi.org\/10.1142\/s0218194096000119","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,6]]}}}