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

Detalles Bibliográficos
Publicado:	2013
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:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v39_n7_p975_Sibay 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	paper:paper_00985589_v39_n7_p975_Sibay
record_format	dspace
spelling	paper:paper_00985589_v39_n7_p975_Sibay2023-06-08T15:09:57Z Synthesizing modal transition systems from triggered scenarios 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. 2013 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v39_n7_p975_Sibay 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 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.
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
publishDate	2013
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v39_n7_p975_Sibay http://hdl.handle.net/20.500.12110/paper_00985589_v39_n7_p975_Sibay
_version_	1768544359804829696

Synthesizing modal transition systems from triggered scenarios

Ejemplares similares