An approach to specification, verification and construction of PLC programs for discrete problems is proposed.For the specification of the program behavior, we use the linear-time temporal logic LTL.Programming is carried out in ST, IL and LD languages according to an LTL-specification.The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV.A new approach to PLCprogramming is shown by an example.For a discrete problem, we give an ST-program, its LTL-specification and an SMV-model.
We present a model-driven engineering approach that enables to take energy consumption into account during the development of embedded software. In this approach we address all the constituents of a typical modern embedded solution (mechanics, communication and computation subsystems) through the application of different modelling technologies. This makes it possible to evaluate the implications of different software and system architectures in the system’s energy consumption. Additionally it facilitates the exploration of the design space without having to prototype each candidate solution. We also provide details on the application of this approach to the development of a medical grade compression stocking and the benefits this approach has brought to the project currently developing this system.
The paper presents a work-in-progress project on construction of a security facility that protects trusted application from malware residing at any privilege level of an OS, including OS kernel. The approach is based on the Sevigator project that used KVM to protect applications running in QEMU. The presented project is a port of Sevigator to much smaller trusted computing base of a bare-metal hypervisor.
The paper presents a lightweight approach to static data race detection. It is based on the Lockset one, but it implements several simplifications that are aimed to reduce amount of false alarms. The approach is implemented on top of CPAchecker tool and its evaluation is in progress. The main target of our research and evaluation is operating system kernels but the approach can be applied to analysis of other programs as well.
We study the verification of the soundness property for workflow nets extended with resources. A workflow is sound if it terminates properly (no deadlocks and livelocks are possible). A class of resource-constrained workflow nets (RCWF-nets) is considered, where resources can be used by a process instance, but cannot be created or spent. Two sound RCWF-net, using the same set of resources, can be put in parallel. This parallel composition in some cases may produce additional deadlocks. A problem of deadlock avoidance in parallel workflows is studied, some methods of deadlock search and control are presented.
Errors in critically important systems may become very expensive. If such systems must provide confidentiality when working with some critically important data such as classified information or private know-how, an error cost may become difficult to evaluate. For these systems, formal verification methods should be used to prove they are error-free. In the paper, a case of formal verification of such system – a Linux kernel security module – is considered the chosen toolset, the verification process workflow are reviewed, along with some auxiliary tools required for this process and developed by the authors.
—Time Petri nets are an extension of Petri nets formalism with time specifications on transitions. The formalism is convenient for model distributed systems and enables capturing the time characteristics of distributed system activities. The primary tool for models behaviour understanding is reachability graph. In [10] the algorithm for constructing Time Petri net reachability graph was suggested. It is based on essential states, but the number of states in the resultant net reachability graph increases when time specification are scaled up, while the behaviour of the net is invariant under time specification scaling. We study the modification of this algorithm that allows to build Time Petri nets reachability graphs more efficiently using common divisors of the time specification in the components of a Time Petri net.
Overlapped executable code is an attractive artifact of obfuscation technology not yet widely covered and researched.Overlapped code and opaque predicates technologies together allows creation of prominent software obfuscation technologies featuring both obscure executable code and code protected from patching due to hard-to-track relations with other code.The paper provides polynomial algorithm to generate overlapped executable code using LLVM framework and discuss results of the generation implementation.
activities. For this purpose, each low-level activity in the log is replaced by a name of the subprocess (an abstract activity) it belongs to. Hence we get a log with ”stuttering” abstract activities. This transformation is implemented by the method toHighLevel(), schematically presented in Algorithm 1. Data: lowlevellog — a list of low-level activities, hlaction — a set of high-level activities, where for each high-level activity is stored information about its partition into subsets of low-level activities. Result: highlevellog — a high-level event log. i←− 0; highlevellog ←− ∅; currentLowAction←− lowlevellog[i] while i < lowlevellog.size do // search of high-level activity, // subsets of which contains this // low-level activity currentHighAction←− search(hlaction, currentLowAction); if currentHighAction 6= ∅ then // check of condition that // low-level activity is included // to partition of the current // high-level action while i < lowlevellog.size and currentHighAction.contains(currentLowAction) do i←− i+ 1; end highlevellog.add(currentHighAction); end end return highlevellog; Algorithm 1: Method toHighLevel(), transforming a lowlevel log into a log over abstract activities After converting the refined log into notations of the abstract model we get a new log, which is a multiset of sequences of abstract activities. But this still can not be used for the conformance checking because of stuttering actions. Moreover, when we have two concurrent subprocesses, represented by two concurrent abstract activities in an abstract model, stuttering sequences may interleave. To overcome this ai ... ... p
The work describes the problem of detecting and highlighting text in images. For the comparison, it contains the existing methods to solve this problem, advantages and disadvantages of them and, as a result, own approach to solving the task is proposed.
String-embedded language transformation is one of the problems which can be faced during database and information system migration.The conventional solution which is provided by a number of tools is based on run-time translation.We present a static abstract translation approach which originates from the abstract parsing technique [9] initially developed for syntax analysis of string-embedded languages.We present abstract translation algorithm and some optimization techniques, and discuss the results of its evaluation on a real-world industrial application.
Nowadays a lot of various test generation tools are developed and applied to create tests for both software applications and hardware designs.Taking into account the size and complexity of modern projects, there is an urgent need for "smart" tools that would help maximize test coverage and keep the required effort and time to a minimum.Despite the fact that each project is unique in some sense, there is a set of common generation techniques that are applied in a wide range of projects (random tests, combinatorial tests, tests for corner cases, etc).In addition, projects belonging to specific domains tend to share similar test cases or use similar heuristics to generate them.A natural way to improve the quality of testing is to make the most of the experience gained working on different projects or performing testing at different stages of the same project.To achieve this goal, a knowledgebase holding information relevant to test generation would be of a great help.This would facilitate reuse of test cases and generation algorithms and would allow sharing knowledge of "interesting" situations that can occur in a system under test.The paper proposes a concept of a knowledgebase for test generation that can be used in a wide range of test generation tools.At ISPRAS, it is applied in test program generation tools that create test programs for microprocessors.The knowledgebase is designed to store information on widely used test generation techniques and test situations that can occur in a microprocessor design under verification.
Hardware development processes include verification as one of the most important part.Verification is very often done in simulation-based way.After comparison of design behavior and its reference model behavior, the verdict about their correspondence appears.It is very useful to have some means of analyzing potential inconsistency of their output data.It is exactly the subject of this work to supply verification engineers with a method and a back-end tool for diagnostics of incorrect behavior using wave diagrams and reaction trace analysis based on recombination of reaction traces.
The article is devoted to the problem of applying the formal data mining toolforecastingfor the developing of new software and for reengineering the present software.We propose the algorithm adjustments of the time series forecasting.This algorithm takes into account the dependence of the current state of time series from the previous one, the influence of basic fuzzy projected trends in the time series.The proposed algorithm expands the opportunities of time series short-term forecasting on the base of fuzzy trends, as the historical software time series are of small length.The proposed algorithm was examined experimentally and showed the efficiency
Process mining is a relatively new research area aiming to extract process models from event logs of real systems.A lot of new approaches and algorithms are developed in this field.Researches and developers usually have a need to test end evaluate the newly constructed algorithms.In this paper we propose a new approach for generation of event logs.It serves to facilitate the process of evaluation and testing.Presented approach allows to generate event logs, and sets of event logs to support a large scale testing in a more automated manner.Another feature of the approach is a generation of event logs with noise.This feature allows to simulate real-life system execution with inefficiencies, drawbacks, and crashes.In this work we also consider other existing approaches.Their forces and weaknesses are shown.The approach presented as well as the corresponding tool can be widely used in the research and development process.
DPMine generic purpose workflow language is rooted in DPMine/P scientific workflow language and a set of plug-ins for ProM which originally were developed for convenient piping of different plug-ins within ProM framework.DPMine/C is a new version of DPMine workflow language and a C++ library.The main language concept was complemented by comprehensive analysis of DPMine/C model execution semantics.This paper also discusses approaches to the block types extension concept relying on development of new block type classes and customization of the model storage subsystem.Finally, we show an approach for implementation of a GUI frontend.
This work is dedicated to one of the most urgent problems in the field of process mining. Process mining is a technique that offers plenty of methods for the discovery and analysis of business processes based on event logs. However, there is a lack of real process models and event logs, which can be used to verify the methods developed to achieve process mining goals. Hence, there is a need in an instrument that would generate process models and logs, thus allowing verification of the process mining discovery algorithms. This aim can be reached by the creation of a model and log generator. In this paper a possible solution for the creation of such a generator will be proposed. Namely, it is the generation of process models and event logs using the rules of graph grammars on the example of structured workflow nets. The approach proposed is based on the creation of grammar rules to generate a model and an event log, which fits this model. The evaluation of the process discovery algorithms will be available due to the presence of initial models and event logs generated on the basis of these models. The tools used to perform this work are publicly available. This paper is the research-in-progress, which is conducted in frame of master’s thesis in the field of software engineering.
Nowadays models which are used in the avionics (aviation electronics) development are large and can contain complex behaviour specifications, especially on early stages. This leads to high requirements to simulators which are used for such models analyses. Existing open-source simulators are not applicable or not effective in application on such models. An architecture of a discrete-event simulator using continuations approach for avionics models analysis is suggested.
The paper describes an approach to semantic indexing of electronic documents based on ontology that describes the structure, type of document and its contents. In addition, existing ontology descriptions of documents are considered and the differences between the proposed multidimensional ontology from them are described. The solution of the problem of analysis of administrative regulations is described as an application of the approach. An algorithm for implementing semantic indexing based on multi-agent paradigm is proposed.
In this paper, we consider the problem of test derivation based on an Extended Finite State Machine EFSM) that is widely used for describing the behavior of telecommunication protocols and software. An EFSM augments a classical Finite State Machine (FSM) with context variables, input/output parameters and predicates. Tests based on various coverage criteria for EFSMs do not capture many functional faults and thus, there is a strong need for tests checking functional properties. Moreover, since there are no constructive necessary and sufficient conditions for checking whether two arbitrary EFSMs are equivalent, most methods are based on some kind of a transition tour, despite of the fact that such methods do not provide test suites with the guaranteed fault coverage. Given possibly nondeterministic and partial EFSM, we consider a transition tour of an FSM obtained by the simulation of the initial EFSM and provide some experimental results that such a test suite detects a number of inconsistencies in available protocol implementations with respect to protocol specifications. Since a transition tour augmented with state identifiers is known to have the higher fault coverage, we also discuss how state identifiers can be generated without facing the state explosion problem. Correspondingly, we consider FSM slices that are obtained by deleting from the initial EFSM all the context variables and possibly, input and output parameters. As the obtained FSM can be nondeterministic, a state identifier should contain separating sequences for pairs of states and we adapt the known techniques for deriving separating sequences for nonobservable partial FSMs
