Automated Software Engineering

Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neither can specify structured properties that refer to the call stack of the program. While context-free grammars (CFGs) are expressive and well-understood, existing techniques for monitoring CFGs generate large runtime overhead in real-life applications. This paper demonstrates that monitoring parametric CFGs is practical (with overhead on the order of 12% or lower in most cases). We present a monitor synthesis algorithm for CFGs based on an LR(1) parsing algorithm, modified to account for good prefix matching. In addition, a logic-independent mechanism is introduced to support matching against the suffixes of execution traces.

Ouni et al. “Maintainability defects detection and correction: a multi-objective approach” proposed a search-based approach for generating optimal refactoring sequences. They estimated the size of the search space for the refactoring scheduling problem using a formulation that is incorrect; the search space is estimated to be too much larger than it is. We provide in this paper the exact expression for computing the number of possible refactoring sequences of a software system. This could be useful for researchers and practitioners interested in developing new approaches to automate refactoring.

Developers of software product families and maintainers of “legacy” software can benefit from the ability to automatically extract a correctly functioning subset of the code of a system that performs a desired subset of its behaviors. This article introduces a technique for automatic subsetting based on computing asimultaneous dynamic program slice of the code for a set of representative inputs. I show first why the naive approach (unioning traditional dynamic slices) fails, then give an abstract algorithm that succeeds in any slicing framework satisfying certain (mild) assumptions. Experiments using an implementation within the ISAT environment indicate that the algorithm consistently produces significantly smaller subsets than three competing approaches. I also discuss how to characterize the subset's correctness on inputs of interest outside the set used to compute the slice.

Các ứng dụng di động phổ biến nhận được hàng triệu đánh giá từ người dùng. Những đánh giá này chứa đựng thông tin quan trọng cho việc bảo trì phần mềm, chẳng hạn như báo cáo lỗi và các đề xuất cải tiến. Thông tin từ các đánh giá này là một nguồn kiến thức giá trị cho kỹ thuật yêu cầu phần mềm, vì phân tích đánh giá ứng dụng giúp đưa ra quyết định chiến lược để cải thiện chất lượng ứng dụng. Tuy nhiên, do lượng văn bản lớn, việc trích xuất thông tin liên quan bằng tay là một nhiệm vụ không khả thi. Khai thác ý kiến là lĩnh vực nghiên cứu nhằm phân tích cảm xúc và tâm trạng của con người thông qua ý kiến được bày tỏ trên web, chẳng hạn như mạng xã hội, diễn đàn và các nền tảng cộng đồng để giới thiệu sản phẩm và dịch vụ. Trong bài báo này, chúng tôi nghiên cứu khai thác ý kiến cho các đánh giá ứng dụng. Đặc biệt, chúng tôi so sánh các kỹ thuật đại diện văn bản cho phân loại, phân tích cảm xúc, và dự đoán tiện ích từ các đánh giá ứng dụng. Chúng tôi thảo luận và đánh giá các kỹ thuật khác nhau cho việc đại diện văn bản của các đánh giá, từ mô hình Bag-of-Words (BoW) truyền thống đến các mô hình Ngôn Ngữ Mạng Nơ-rôn (NLM) hiện đại nhất. Kết quả của chúng tôi cho thấy rằng mô hình Bag-of-Words truyền thống, kết hợp với phân tích cẩn thận các kỹ thuật tiền xử lý văn bản, vẫn có khả năng cạnh tranh cao. Nó đạt được kết quả gần với NLM trong các nhiệm vụ phân loại, phân tích cảm xúc, và dự đoán tiện ích. Tuy nhiên, NLM chứng minh là có lợi thế hơn vì chúng đạt được hiệu suất rất cạnh tranh trong tất cả các nhiệm vụ dự đoán được đề cập trong công việc này, cung cấp sự giảm chiều đáng kể, và xử lý tốt hơn với sự gần gũi về mặt ngữ nghĩa giữa các văn bản đánh giá.

In the model-based development context, metamodel-based languages are increasingly being defined and adopted either for general purposes or for specific domains of interest. However, meta-languages such as the MOF (Meta Object Facility)—combined with the OCL (Object Constraint Language) for expressing constraints—used to specify metamodels focus on structural and static semantics but have no built-in support for specifying behavioral semantics. This paper introduces a formal semantic framework for the definition of the semantics of metamodel-based languages. Using metamodelling principles, we propose several techniques, some based on the translational approach while others based on the weaving approach, all showing how the Abstract State Machine formal method can be integrated with current metamodel engineering environments to endow language metamodels with precise and executable semantics. We exemplify the use of our semantic framework by applying the proposed techniques to the OMG metamodelling framework for the behaviour specification of the Finite State Machines provided in terms of a metamodel.

It is shown, how the object-oriented programming paradigm has been combined with automatic program construction in the NUT system: type information extracted from a class specification is being used for automatic construction of methods for the class. Special compute-messages are introduced as requests for program synthesis which can be done statically or dynamically. Particular features of the specification language which support the program synthesis are considered and applications of this method are outlined.

The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers, proof checkers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle big states, and partial order and symmetry reduction, slicing, abstraction, and runtime analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, runtime analysis, and slicing with model checking.

We present a new approach for creating repositories of real software faults. We have developed a tool, the Automatic Fault IDentification Tool (AFID), that implements this approach. AFID records both a fault revealing test case and a faulty version of the source code for any crashing faults that the developer discovers and a fault correcting source code change for any crashing faults that the developer corrects. The test cases are a significant contribution, because they enable new research that explores the dynamic behaviors of the software faults. AFID uses an operating system level monitoring mechanism to monitor both the compilation and execution of the application. This technique makes it straightforward for AFID to support a wide range of programming languages and compilers. We present our experience using AFID in a controlled case study and in a real development environment to collect software faults in the internal development of our group’s compiler. The case studies collected several real software faults and validated the basic approach. The longer term internal study revealed weaknesses in using the original version of AFID for real development. This experience led to a number of refinements to the tool for use in real software development. We have collected over 20 real software faults in large programs and continue to collect software faults.

We describe a proof method that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This method provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This method makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate it with parts of a substantial example—the synthesis of a unification algorithm.