Innovations in Systems and Software Engineering

Nhiều hệ thống quan trọng trong thực tế được mô tả bằng các mô hình lớn và thể hiện hành vi vừa xác suất vừa không xác định. Việc kiểm chứng những hệ thống như vậy đòi hỏi các kỹ thuật để tránh vấn đề bùng nổ không gian trạng thái. Kiểm tra mô hình hình tượng và xác minh thành phần chẳng hạn như lập luận giả thiết-đảm bảo là hai kỹ thuật hứa hẹn để vượt qua rào cản này. Trong bài báo này, chúng tôi đề xuất một phương pháp xác minh thành phần hình tượng xác suất (PSCV) để kiểm chứng các hệ thống xác suất, trong đó mỗi thành phần là một quá trình quyết định Markov (MDP). PSCV bắt đầu bằng cách mã hóa ngầm các thành phần của hệ thống bằng cách sử dụng cấu trúc dữ liệu gọn. Để thiết lập quá trình xác minh thành phần hình tượng, chúng tôi đề xuất một quy tắc lập luận giả thiết-đảm bảo hình tượng chính xác và đầy đủ. Để đạt được tính đầy đủ của quy tắc lập luận giả thiết-đảm bảo hình tượng, chúng tôi đề xuất mô hình hóa các giả thiết bằng việc sử dụng MDP khoảng. Thêm vào đó, chúng tôi đưa ra một thuật toán học MTBDD hình tượng để tự động tạo ra các giả thiết hình tượng. Hơn nữa, chúng tôi đề xuất sử dụng quan hệ nguyên nhân để tạo ra các phản ví dụ nhỏ nhằm làm tinh chỉnh các giả thiết. Kết quả thực nghiệm cho thấy triển vọng hứa hẹn cho phương pháp hình tượng xác suất thành phần của chúng tôi.

The topic of this paper is the determinization problem of $$\omega $$ -automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

It may appear that for software systems that require strict real-time behavior, the idea of incorporating self-management (and specifically concepts from Autonomic Computing) may add the burden of excessive additional functionality and overhead. However, our experience is that, not only does real-time software benefit from autonomicity, but also the Autonomic Computing initiative (like other initiatives aiming at self-management) requires the expertise of the real-time community in order to achieve its overarching vision. In particular, there are emerging classes of real-time systems for which incorporation of self-management is absolutely essential in order to implement all of the requirements of the system, and in particular the timing requirements.

In this paper we describe a modeling framework aimed at facilitating the customization and deployment of artificial intelligence (AI) scheduling technology in real-world contexts. Specifically, we describe an architecture aimed at facilitating software product line development in the context of scheduling systems. The framework is based on two layers of abstraction: a first layer providing an interface with the scheduling technology, on top of which we define a formalism to abstract domain-specific concepts. We show how this two-layer modeling framework provides a versatile formalism for defining user-oriented problem abstractions, which is pivotal for facilitating interaction between domain experts and technologists. Moreover, we describe a graphical user interface (GUI)-enhanced tool which allows the domain expert to interact with the underlying core scheduling technology in domain-specific terms. This is achieved by automatically instantiating an abstract GUI template on top of the second modeling layer.

This article describes symbolic approximation, a theoretical foundation for techniques evolved for large-scale verification – in particular, for post hoc verification of the C code in large-scale open-source projects such as the Linux kernel. The corresponding toolset’s increasing maturity means that it is now capable of treating millions of lines of C code source in a few hours on very modest support platforms. In order to explicitly manage the state-space-explosion problem that bedevils model-checking approaches, we work with approximations to programs in a symbolic domain where approximation has a well-defined meaning. A more approximate program means being able to say less about what the program does, which means weaker logic for reasoning about the program. So we adjust the approximation by adjusting the applied logic. That guarantees a safe approximation (one which may generate false alarms but no false negatives) provided the logic used is weaker than the exact logic of C. We choose the logic to suit the analysis.