Compositional verification, such as the technique of assume-guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion problem associated with model checking. However, obtaining the appropriate assumption for AGR is always a highly mental challenge, especially in the case of timed systems. In this paper, we propose a learning-based compositional verification framework for deterministic timed automata. In this framework, a modified learning algorithm is used to automatically construct the assumption in the form of a deterministic one-clock timed automaton, and an effective scheme is implemented to obtain the clock reset information for the assumption learning. We prove the correctness and termination of the framework and present two kinds of improvements to speed up the verification. We discuss the results of our experiments to evaluate the scalability and effectiveness of the framework. The results show that the framework we propose can reduce state space effectively, and it outperforms traditional monolithic model checking for most cases.

AUTOSAR (AUTomotive Open System ARchitecture) is a development partnership whose primary goal is the standardization of basic system functions and functional interfaces for electronic control units in automobiles. As an open specification, its layered software architecture promotes the interoperability of real-time embedded vehicle systems and components. It also opens up the possibility of formal modelling and verification approaches, centred around the specification, that can be used to support analysis in the early stages of design. In this paper, we describe a methodology and associated tool, called A2A, that automatically models systems defined by the AUTOSAR specifications as timed au-tomata, and then verifies their timing properties using UPPAAL. It contains 22 groups of timed automata templates, together with two auxiliary test templates, that model the AUTOSAR architecture and timing properties, allowing time-related behaviours to be extracted from the three-layer architecture, i.e., the AUTOSAR Software, AUTOSAR Runtime Environment, and Basic Software layers, and templates to be automatically instantiated. The timing properties are specified using timed computation tree logic (TCTL) in UPPAAL to verify the system model. We demonstrate the capabilities of the methodology by applying it to an AUTOSAR architecture that describes an internal vehicle light control system, thereby showing its effectiveness. (c) 2023 Elsevier Inc. All rights reserved.

时间自动机的模型学习算法旨在通过提供输入和观察输出构建软硬件系统的形式化模型.确定性单时钟时间自动机的学习是其中的一个重要研究方向,但是该算法具有一定的局限性,在状态较多时学习速度较慢,很难应用到复杂的系统中.由此,提出了一种改进的学习算法,使用逻辑时间分类树代替逻辑时间观察表作为学习算法的内部数据结构,有效地减少了成员查询次数,降低了算法的空间复杂度,并能够高效率地构建假设自动机.最后进行了相关实验,实验结果表明,提出的改进算法减少了60％左右的成员查询和5％左右的等价查询.同时在该实验中,改进算法的学习速度最高可提高45倍以上.

Traditional machine learning algorithms heavily depend on training data. In order to reduce the amount of training data, active learning is proposed to find out the critical data, which place more important roles against other data. The active learning algorithm is also used to learn real-time automaton(RTA). However, a huge number of membership queries and equivalence queries are generated in the learning process. In this paper, We design a new data structure to store the information obtained by membership queries. This data structure is a kind of tree structure, and improve the efficiency of the active learning for real-time RTA because this structure can process counter-examples effectively. Some experiments are conducted, and the results show that the algorithm can significantly reduce the number of membership queries without increasing the equivalence queries numbers. From the data point of view, our algorithm reduces the number of membership queries by 50% and the execution time by 80%.