TY - GEN
T1 - From requirements to specifications
AU - Plock, Cory
AU - Goldberg, Benjamin
AU - Zuck, Lenore
PY - 2005
Y1 - 2005
N2 - Live Sequence Charts (LSCs) provide a formal visual framework for creating scenario-based requirements for reactive systems. An LSC imposes a partial order over a set of events, such as the sending or receiving of messages. Each event is associated with a liveness property, indicating whether it can or must occur. Time extensions can further specify when these events should occur. An individual LSC tells a story about particular fragment of system behavior, whereas LSC specifications - a finite set of LSCs - collectively define the total behavior. An LSC specification may require that more than one distinct scenario, or multiple instances of the same scenario, execute concurrently. It is natural to ask whether LSC specifications can be synthesized into formal languages. Previous work offers translations from untimed LSCs to finite state machines, and from single (non-concurrent) LSCs to timed automata. Here, we show that LSC specifications with concurrency can also be expressed as a timed automata.
AB - Live Sequence Charts (LSCs) provide a formal visual framework for creating scenario-based requirements for reactive systems. An LSC imposes a partial order over a set of events, such as the sending or receiving of messages. Each event is associated with a liveness property, indicating whether it can or must occur. Time extensions can further specify when these events should occur. An individual LSC tells a story about particular fragment of system behavior, whereas LSC specifications - a finite set of LSCs - collectively define the total behavior. An LSC specification may require that more than one distinct scenario, or multiple instances of the same scenario, execute concurrently. It is natural to ask whether LSC specifications can be synthesized into formal languages. Previous work offers translations from untimed LSCs to finite state machines, and from single (non-concurrent) LSCs to timed automata. Here, we show that LSC specifications with concurrency can also be expressed as a timed automata.
UR - http://www.scopus.com/inward/record.url?scp=28344452783&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=28344452783&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:28344452783
SN - 0769523080
SN - 9780769523088
T3 - Proceedings - 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECS 2005
SP - 183
EP - 190
BT - Proceedings - 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECS 2005
A2 - Rozenblit, J.
A2 - O'Neill, T.
A2 - Peng, J.
T2 - Proceedings - 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECS 2005
Y2 - 4 April 2005 through 7 April 2005
ER -