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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Sibay, G.E., Braberman, V., Uchitel, S., Kramer, J.
Formato: JOUR
Materias:
MTS
partial behavior models
Scenarios
synthesis
Labeled transition systems
Modal Transition Systems
Operational behavior
Partial behavior models
Scenario-based languages
Scenario-based specifications
Flowcharting
Semantics
Specification languages
Synthesis (chemical)
Specifications
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_00985589_v39_n7_p975_Sibay
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
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

Ejemplares similares