WASPI 2018- Proceedings of the 1st ACM SIGSOFT International Workshop on Automated Specification Inference

During the development of an embedded system, state transition models are frequently used for modeling at several abstraction levels. Unfortunately, specification documents including such model are often lost or not up to date during maintenance/reuse. Based on our experience in industrial collaboration, we present Micro State Transition Table (MSTT) to help developers understanding embedded code based on a fine-grained state transition model. We also discuss the challenges of static recovery of an MSTT.

Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior -- its contract -- is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.

Creativity can often be seen in artistic productions when artists use their imagination to create original and novel work. However, the importance of creativity is being broadly recognized in various areas. Recently, the requirements engineering (RE) research community has been paying more attention to the matter of capturing and generating creative requirements as it plays a pivotal role in a software system sustainability. To further advance the literature, in this paper, we propose a automated system to alleviate creative feature generation by using a Hidden Markov Model with requirements data scraped from Google Play. To evaluate the performance of the system, We experiment our system in two settings, generating features from a specific application domain (i.e., Messaging platform) and from a mixed domains of successful applications including Google Chrome and Dropbox. The results offer encouraging insights on how our system can support capturing creative requirements and aid the development of more advanced software feature generators.

The programmers utilize APIs provided by frameworks and libraries to avoid reinventing the wheel and API specifications aid them to fully understand and adequately use these APIs. This paper introduces "contract-based typestate specifications", a new kind ofspecification for documenting programs. Prior work has focused on two kinds of specifications, namely behavioral and temporal specifications. These specifications either target the constraints of API method invocations or, the usage order of API methods to ensure normal behavior. Consequentially, these two types of specifications are treated independently. Another challenge for these state-of-art specifications lies in the form of limited expressiveness to the designers’ intention, as these are unable to demonstrate all the valid choices under same or different constraints. Contract-based typestate specifications capture the essence of behavioral and temporal specifications, yet provide better understanding and ensure valid API usage as required by context, thus providing flexibility of usage.

The preconditions of an API method are constraints on the states of its receiver object and arguments intended by the library designer(s) to correctly invoke it in the client code. There have been two main kinds of approaches for automatically inferring API preconditions. The first kind of approaches mines the frequently checked conditions guarding the API usages in the client code and generalize them into preconditions. The second kind of approaches analyzes the implementation of the API to compute preconditions.

In this paper, we report an observation that the usage-based approach often produces preconditions stronger than those intended while the implementation-based produces weaker ones. Our finding calls for a new direction of integrating those kinds of precondition inference approaches and refinement solutions to reduce the differences between sets of inferred preconditions.