Synthesizing modal transition systems from triggered scenarios
Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional univer...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_00985589_v39_n7_p975_Sibay |
| Aporte de: |
| id |
todo:paper_00985589_v39_n7_p975_Sibay |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_00985589_v39_n7_p975_Sibay2023-10-03T14:56:58Z Synthesizing modal transition systems from triggered scenarios Sibay, G.E. Braberman, V. Uchitel, S. Kramer, J. MTS partial behavior models Scenarios synthesis Labeled transition systems Modal Transition Systems MTS Operational behavior Partial behavior models Scenario-based languages Scenario-based specifications Scenarios Flowcharting Semantics Specification languages Synthesis (chemical) Specifications Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration. © 1976-2012 IEEE. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00985589_v39_n7_p975_Sibay |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
MTS partial behavior models Scenarios synthesis Labeled transition systems Modal Transition Systems MTS Operational behavior Partial behavior models Scenario-based languages Scenario-based specifications Scenarios Flowcharting Semantics Specification languages Synthesis (chemical) Specifications |
| spellingShingle |
MTS partial behavior models Scenarios synthesis Labeled transition systems Modal Transition Systems MTS Operational behavior Partial behavior models Scenario-based languages Scenario-based specifications Scenarios Flowcharting Semantics Specification languages Synthesis (chemical) Specifications Sibay, G.E. Braberman, V. Uchitel, S. Kramer, J. Synthesizing modal transition systems from triggered scenarios |
| topic_facet |
MTS partial behavior models Scenarios synthesis Labeled transition systems Modal Transition Systems MTS Operational behavior Partial behavior models Scenario-based languages Scenario-based specifications Scenarios Flowcharting Semantics Specification languages Synthesis (chemical) Specifications |
| description |
Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration. © 1976-2012 IEEE. |
| format |
JOUR |
| author |
Sibay, G.E. Braberman, V. Uchitel, S. Kramer, J. |
| author_facet |
Sibay, G.E. Braberman, V. Uchitel, S. Kramer, J. |
| author_sort |
Sibay, G.E. |
| title |
Synthesizing modal transition systems from triggered scenarios |
| title_short |
Synthesizing modal transition systems from triggered scenarios |
| title_full |
Synthesizing modal transition systems from triggered scenarios |
| title_fullStr |
Synthesizing modal transition systems from triggered scenarios |
| title_full_unstemmed |
Synthesizing modal transition systems from triggered scenarios |
| title_sort |
synthesizing modal transition systems from triggered scenarios |
| url |
http://hdl.handle.net/20.500.12110/paper_00985589_v39_n7_p975_Sibay |
| work_keys_str_mv |
AT sibayge synthesizingmodaltransitionsystemsfromtriggeredscenarios AT brabermanv synthesizingmodaltransitionsystemsfromtriggeredscenarios AT uchitels synthesizingmodaltransitionsystemsfromtriggeredscenarios AT kramerj synthesizingmodaltransitionsystemsfromtriggeredscenarios |
| _version_ |
1807316763643215872 |