Scenario-Based Programming is a methodology for modeling and constructing complex reactive systems from simple, stand-alone building blocks, called scenarios. These scenarios are designed to model different traits of the system, and can be interwoven together and executed to produce cohesive system behavior. Existing execution frameworks for scenario-based programs allow scenarios to specify their view of what the system must, may, or must not do only through very strict interfaces. This limits the methodology's expressive power and often prevents users from modeling certain complex requirements. Here, we propose to extend Scenario-Based Programming's execution mechanism to allow scenarios to specify how the system should behave using rich logical constraints. We then leverage modern constraint solvers (such as SAT or SMT solvers) to resolve these constraints at every step of running the system, towards yielding the desired overall system behavior. We provide an implementation of our approach and demonstrate its applicability to various systems that could not be easily modeled in an executable manner by existing Scenario-Based approaches.
翻译:基于情景的方案编制是一种从简单、独立的构件中建模和构建复杂反应系统的方法,称为假设情景。这些假设情景旨在模拟系统的不同特性,可以相互交织,并用于形成系统行为的一致性。基于情景的现有方案执行框架允许基于情景的现有方案执行框架具体说明系统必须、可能或不能仅仅通过非常严格的界面来做哪些工作。这限制了方法的表达力,并常常阻止用户建模某些复杂要求。在这里,我们提议扩大基于情景的方案编制执行机制,以便让假设情景能够说明系统应如何使用丰富的逻辑限制来行事。然后我们利用现代制约解决器(如SAT或SMT解答器),在运行系统的每一个阶段解决这些制约因素,从而产生理想的整体系统行为。我们提供我们的方法的实施,并展示其适用于各种系统的适用性,而现有基于情景的方法无法以易于执行的方式建模。