System and Software Engineering is about implementing “what the user wanted” (colloquial phrasing borrowed from the famous tree-swing cartoon; seeFig. 1). We begin this paper by revisiting briefly the decades-long continuous pursuit of answers to some of the underlying engineering challenges, carried out by the first-listed author and his colleagues. Along this road, concepts like executable specifications, visual formalisms, hierarchies, abstractions, and scenarios play major roles. We then reflect upon the observation that the very discovery of “what the user wanted,” which often appears to require only elicitation in some structured requirement engineering process, actually poses significant challenges of its own. Documenting in advance the requirements for a real-world reactive system, such as an autonomous vehicle—and more generally, producing a textual and visual description of what a system does or needs to do—is becoming ever harder, and in certain cases impossible. Furthermore, producing quality specifications is critical not only for eventually satisfying the user, but for early detection of critical faults. We conclude by outlining future approaches and tools that may be able to mitigate the severity of this issue.

Artificial intelligence (AI) techniques, including, e.g., machine learning, multi-agent collaboration, planning, and heuristic search, are emerging as ever-stronger tools for solving hard problems in real-world applications. Executable specification techniques (ES), including, e.g., Statecharts and scenario-based programming, is a promising development approach, offering intuitiveness, ease of enhancement, compositionality, and amenability to formal analysis. We propose an approach for integrating AI and ES techniques in developing complex intelligent systems, which can greatly simplify agile/spiral development and maintenance processes. The approach calls for automated detection of whether certain goals and sub-goals are met; a clear division between sub-goals solved with AI and those solved with ES; compositional and incremental addition of AI-based or ES-based components, each focusing on a particular gap between a current capability and a well-stated goal; and, iterative refinement of sub-goals solved with AI into smaller sub-sub-goals where some are solved with ES, and some with AI. We describe the principles of the approach and its advantages, as well as key challenges and suggestions for how to tackle them.

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.

During system development, external reviewers, especially ones with expertise in the problem domain or in system and software engineering (SE), often contribute insights that up to that point were not noticed by the engineers and other project stakeholders. These reviewers apparently do so by employing special human competencies that presently are not, or even cannot be, automated. Consider, for example, the competencies that enable the following review comments about a home-assistant robot: (a) during code review: "I see that the robot can defers command execution until it charges its battery for the task; When done charging, does the robot check if the action is still needed?"; (b) following a demo: "Will the robot trip over a thin ,transparent phone cord?"; and (c) "Some clear voice commands had to be repeated. Perhaps sometimes the robot isn't listening?".

We present a development environment that proactively and interactively assists the software engineer in modeling complex reactive systems. Our framework repeatedly analyzes models of the system under development at various levels of abstraction, and then reasons about these models in order to detect possible errors and to derive emergent properties of interest. Upon request, the environment can then augment the system model in order to repair or avoid detected behavior that is undesired, or instrument it in order to monitor the execution for certain behaviors. Specialized automated and human-assisted techniques are incorporated to direct and prioritize the analysis and related tasks, based on the relevance of the observed properties and the expected impact of actions to be taken. Our development environment is an initial step in the direction of the very recent Wise Computing vision, which calls for turning the computer (namely, the development environment) into an equal member of the development team: knowledgeable, independent, concerned and proactively involved in the development process. Our tool is implemented within the context of behavioral programming (BP), a scenario-based modeling approach, where components are aligned with how humans often describe desired system behavior. Thus, our work further enhances the naturalness and incrementality of developing in BP.

The ability to create succinct programs is a central criterion for comparing programming and specification methods. Specifically, approaches to concurrent programming can often be thought of as idioms for the composition of automata, and as such they can then be compared using the standard and natural measure for the complexity of automata, descriptive succinctness. This measure captures the size of the automata that the evaluated approach needs for expressing the languages under discussion. The significance of this metric lies, among other things, in its impact on software reliability, maintainability, reusability and simplicity, and on software analysis and verification. Here, we focus on the succinctness afforded by three basic concurrent programming idioms: requesting events, blocking events and waiting for events. We show that a programming model containing all three idioms is exponentially more succinct than non-parallel automata, and that its succinctness is additive to that of classical nondeterministic and "and" automata. We also show that our model is strictly contained in the model of cooperating automata à la statecharts, but that it may provide similar exponential succinctness over non-parallel automata as the more general model - while affording increased encapsulation. We then investigate the contribution of each of the three idioms to the descriptive succinctness of the model as a whole, and show that they each have their unique succinctness advantages that are not subsumed by their counterparts. Our results contribute to a rigorous basis for assessing the complexity of specifying, developing and maintaining complex concurrent software.

In recent years formal verification techniques have become an important part of the development cycle of concurrent software. In order to tackle the state explosion problem and verify larger systems, a great deal of work has been put into improving the scalability of verification tools. In this work, we seek to draw attention to an alternative/complementary approach to improving scalability, which sometimes receives less notice: the effect the concurrent programming model itself has on one’s ability to verify programs encoded within it. Recent work suggests that a suitable choice of model, tailored to the problem at hand, may render the produced software more amenable to verification techniques. We recapitulate some recent and new results demonstrating this effect in programming models for discrete, synchronous reactive systems, and outline some directions for future work. We hope that the paper will trigger additional research on this important topic.

We present a method and a tool for composing a reactive system and for accompanying the development and documentation process with a proof of its correctness. The approach is based on behavioral programming (BP) and the Z3 SMT solver. We show how program verification can be automated and streamlined by combining properties of individual modules, specified and verified separately, with application-independent specifications both of the BP semantics and of general theories. The method may yield an exponential acceleration of the verification process when compared with model-checking the composite application. We show that formalization of properties of independent modules in preparation for the correctness proofs can be useful as documentation for future development. We view this work as a further step towards making formal correctness proofs standard practice in the development of reactive systems, and carried out by programmers at large.

We propose a framework for the development of switched fuzzy systems, in which the discrete characteristics of the mode-switching logic are implemented using the paradigm of behavioral programming: they are coded as independent behavior threads and are interwoven at runtime. We demonstrate how such mode switching enables the simplification of fuzzy rules, and reduces their total number, as well as the number of rules evaluated in a computation cycle. The ability of the behavioral programming approach to describe independent simultaneous aspects of behavior in a modular and incremental manner, which aligns with how people often specify requirements, is shown to complement the intuitive nature of fuzzy logic. Our approach is backed by a Java package that provides an initial infrastructure for implementations.

Scenario-based programming is an approach to software development which calls for developing independent software modules to describe different behaviors that a system should or should not follow, and then coordinating the interwoven execution of these modules at run time. We show that patterns previously shown to exist in programs written in the Scratch environment, which is not specifically scenario oriented, by children who did not have other training, and were not guided to write in a scenario-based manner, are also characteristic to scenario-based programming. These patterns include extremely fine-grain decomposition and bottom-up development. This result suggests that scenario-based programming concepts are "natural" in some ways. Thus, with an appropriate environment and a matching set of tools, scenario-based programming concepts could have an important role in early-stage computer-programming curricula.

System specifications are often structured as collections of scenarios and use-cases that describe desired and forbidden sequences of events. A recently proposed behavioral programming approach, which evolved from the visual language of live sequence charts (LSCs), calls for coding software modules in alignment with such scenarios. We present a methodology and a supporting model-checking tool for verifying behavioral Java programs, without having to first translate them into a specific input language for the model checker. Our method facilitates early discovery of conflicting or under-specified scenarios, which can often be resolved by adding new scenarios rather than by changing existing code. Also, counterexamples provided by the tool are themselves event sequences that can serve directly for refinements and corrections. Our tool reduces the size of the execution state-space using an abstraction that focuses on behaviorally interesting states and treats transitions between them as atomic.

We address the problem of comprehending cause and effect relationships between relatively independent behavior components of a single application. Our focus is on the paradigm of behavioral, scenario-based, programming, as captured by the language of live sequence charts (LSC) or its Java-based counterpart, BPJ. In this programming paradigm, multi-modal behaviors can be specified separately, and are integrated only at run time. We present a tool, with which the user can easily follow the decisions of the collective execution mechanism. It shows the behaviors and events that were executed at each point in time, and those that were delayed or abandoned, as well as the causes and reasons behind these run-time choices. The dynamic effects of such decisions on the system's behavior can be seen easily too.