Открытый доступ
Доступ предоставлен
Только для подписчиков
Том 42, № 4 (2016)
- Год: 2016
- Статей: 6
- URL: https://journal-vniispk.ru/0361-7688/issue/view/10830
Article
“Truly concurrent” and nondeterministic semantics of discrete-time Petri nets
Аннотация
In the paper, a “truly concurrent” and nondeterministic semantics is defined in terms of branching processes of discrete-time Petri nets (DTPNs). These nets may involve infinite numbers of transitions and places, infinite number of tokens in places, and (maximal) steps of concurrent transitions, which allows us to consider this class of DTPNs to be the most powerful class of Petri nets. It is proved that the unfolding (maximal branching process) of the DTPN is the greatest element of a complete lattice constructed on branching processes of DTPNs with step semantics. Moreover, it is shown that this result is true also in the case of maximal transition steps if additional restrictions are imposed on the structure and behavior of the DTPN.
187-197
Comparison of specification decomposition methods in Event-B
Аннотация
Decomposition is an important phase in the design of medium and large-scale systems. Various architectures of software systems and decomposition methods are studied in numerous publications. Presently, formal specifications of software systems are mainly used for experimental purposes; for this reason, their size and complexity are relatively low. As a result, in the development of a nontrivial specification, different approaches to the decomposition should be compared and the most suitable approach should be chosen. In this paper, the experience gained in the deductive verification of the formal specification of the mandatory entity-role model of access and information flows control in Linux (MROSL DP-model) using the formal Event-B method and stepwise refinement technique is analyzed. Two approaches to the refinementbased decomposition of specifications are compared and the sources and features of the complexity of the architecture of the model are investigated.
198-205
Conflict resolution in multi-agent systems with typed relations for ontology population
Аннотация
The paper presents a conflict resolution algorithm for multi-agent systems with agents connected by relations of different types and worth. The result of conflict resolution is a conflict-free set of agents. We apply this algorithm for the ambiguity resolution problem in ontology population based on multiagent natural language text analysis.
206-215
On fuzzy repetitions detection in documentation reuse
Аннотация
Increasing complexity of software documentation calls for additional requirements of document maintenance. Documentation reuse can make a considerable contribution to solve this problem. This paper presents a method for fuzzy repetitions search in software documentation that is based on software clone detection. The search results are used for document refactoring. This paper also presents Documentation Refactoring Toolkit implementing the proposed method and integrated with the DocLine project. The proposed approach is evaluated on documentation packages for a number of open-source projects: Linux Kernel, Zend Framework, Subversion, and DocBook.
216-224
Checking several requirements at once by CEGAR
Аннотация
Currently, static verifiers based on counterexample-guided abstraction refinement (CEGAR) can prove correctness of a program against a specified requirement, find its violation in a program, and stop analysis or exhaust the given resources without producing any useful result. Theoretically, we could use this approach for checking several requirements at once; however, finding of the first violation of some requirement or exhausting resources for some requirement will prevent from checking the program against other requirements. Moreover, if the program contains more than one violation of the requirement, CEGAR will find only the very first violation and may miss potential errors in the program. At the same time, static verifiers perform similar actions during checking of the same program against different requirements, which results in waste of a lot of resources. This paper presents a new CEGAR-based method for software static verification, which is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR checking requirements one by one. To achieve this goal, the suggested method distributes resources over requirements and continues analysis after finding a violation of a requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by five times. The total number of divergent results in comparison with the base CEGAR was about 2%. Having continued the analysis after finding the first violation, this method guarantees that all violations of given requirements are found in 40% of cases, with the number of violations found being 1.5 times greater than in that in the base CEGAR approach.
225-238
Program schemata technique for propositional program logics: A 30-year history
Аннотация
A survey is presented of the so-called program schemata technique for proving the decidability of propositional program logics. This method is based on the reduction to versions of the problem of relative totality for nondeterministic Yanov schemata.
239-256