Статьи журнала - Труды Института системного программирования РАН
Все статьи: 115
A flat chart technique for embedded OS testing
Статья научная
Modern automatic devices are more and more equipped with microcontroller units. The logic of work of the automatic equipment is supported by a number of various embedded software applications, which run under an embedded real-time operating system (OS). The OS reliability is extremely important for correct functionality of the whole automatic system. Therefore, the embedded OS should be tested thoroughly with an appropriate automated test suite. Such test suite for testing of an embedded OS is usually organized as a set of multi-task test applications to be executed in a data-driven manner. The paper features a special language to define the respective testing task logic and the concept of flat charts to efficiently perform an embedded OS execution-based testing. To avoid heavy interpreting of text strings during the test run, the respective test presentation is pre-processed in order to convert the initial string form into a regular array form and thus to increase its efficiency.
Бесплатно
A model checking-based method of functional test generation for HDL descriptions
Статья научная
Automated test generation is a promising direction in hardware verification research area. Functional test generation methods based on models are widespread at the moment. In this paper, a functional test generation method based on model checking is proposed and compared to existing solutions. Automated model extraction from the hardware design’s source code is used. Supported HDLs include VHDL and Verilog. Several kinds of models are used at different steps of the test generation method: guarded action decision diagram (GADD), high-level decision diagram (HLDD) and extended finite-state machine (EFSM). The high-level decision diagram model (which is extracted from the GADD model) is used as a functional model. The extended finite-state machine model is used as a coverage model. The aim of test generation is to cover all the transitions of the extended finite state machine model. Such criterion leads to the high HDL source code coverage. Specifications based on transition and state constraints of the EFSM are extracted for this purpose. Later, the functional model and the specifications are automatically translated into the input format of the nuXmv model checking tool. nuXmv performs model checking and generates counterexamples. These counterexamples are translated to functional tests that can be simulated by the HDL simulator. The proposed method has been implemented as a part of the HDL Retrascope framework. Experiments show that the method can generate shorter tests than the FATE and RETGA methods providing the same or better source code coverage.
Бесплатно
A modified Scrum story points estimation method based on fuzzy logic approach
Статья научная
Several known methods allow to estimate the overall effort(s) to be used up for the software development. The approach based on story points is preferable and quite common in the context of Sсrum agile development methodology. However, it might be rather challenging for people, who are new to this methodology or to a specific Scrum team to estimate the amount of work with story points. The proposed approach involves estimation of features on the basis of linguistic terms that are both habitual and clear for everyone. The presented fuzzy inference system (Mamdani’s model) makes it possible to calculate story points using people’s opinions expressed as sentences in natural language - the study shows empirically that beginners to Scrum methodology consider the proposed approach to be more convenient and easier in use than the ‘plain’ story points estimation. Also, four groups of people with different levels of qualification in Scrum were asked to estimate several features of a certain project using the developed approach and common story points approach to prove the relevance of the approach - it was shown that the results of basic story points estimation for Scrum experts differ slightly from the results revealed by proposed approach, while for Scrum beginners such difference is significant. To the opinion of authors, the proposed approach may allow to adapt to Scrum more smoothly, with better understanding of what is implied by story points, grasping the general idea and learning faster their use in practice. The experimental study conducted as a part of the research has shown results approaching the estimations provided by Scrum experts who have been working in real projects and making use of story points for several years. Continuation of the present work can be associated with intensive studies of more complicated methods of aggregation of the experts’ opinions, analysis of alternative representation forms of confidence degrees in estimates provided as well as the development of plugin for JIRA tracking system.
Бесплатно
A static approach to estimation of execution time of components in AADL models
Статья научная
During development of modern avionics systems and other mission-critical systems modelling is vitally used. Models can be used for checking and validation of developed system, including early validation. Early validation is very important because the cost of errors is raising exponentially depending on the development stage. For modelling of such systems, Architecture Analysis and Design Language (AADL) is widely used. It allows to model both architecture of a developed system and some of behavioral characteristics of its components. In the paper the task of automated model checking for consistency of some behavioral properties is considered. In particular, we focus on the problem of estimation of working time of model components and corresponding between this time and other properties in a model. This problem is close to the worst-case execution time problem (WCET) but it has its own specific in this application. We considered a static approach allowing to work with standard specification of components behaviour in AADL-models with specialized extended finite automata. In the paper peculiarities of used behaviour model (specialized finite automata) were considered including work with time and external events. We considered the problem of working time estimation for such models connected with non-local characteristic of this property. We propose an algorithm for time estimation for such behaviour models. This algorithm was implemented in MASIW framework, a tool for development of AADL-models.
Бесплатно
ADV_SPM - формальные модели политики безопасности на практике
Статья научная
В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.
Бесплатно
Статья научная
Vehicle Routing Problem (VRP) is one of the most widely known questions in a class of combinatorial optimization problems. It is concerned with the optimal design of routes to be used by a fleet of vehicles to serve a set of customers. In this study we analyze Capacitated Vehicle Routing Problem (CVRP) - a subcase of VRP, where the vehicles have a limited capacity. CVRP is mostly aimed at savings in the global transportation costs. The problem is NP-hard, therefore heuristic algorithms which provide near-optimal polynomial-time solutions will be considered instead of the exact ones. The aim of this article is to make a survey on mathematical formulations of CVRP and on methods for solving each type of this problem. The first part presents a general information about the problem and restrictions of this work. In the second part, the classical mathematical formulations of CVRP are described. In the third part, a classification of most popular subcases of CVRP is given, including description of additional constraints with their math formulations. This section also includes most perspective methods that can be applied for solving special types of CVRP. The forth part contains an important note about the most powerful algorithm LKH-3. Finally, the fourth part consists of table with solving techniques for each subproblem and of scheme with basic problems of the CVRP class and their interconnections.
Бесплатно
Applying deep learning to C# call sequence synthesis
Статья научная
Many common programming tasks, like connecting to a database, drawing an image, or reading from a file, are long implemented in various frameworks and are available via corresponding Application Programming Interfaces (APIs). However, to use them, a software engineer must first learn of their existence and then of the correct way to utilize them. Currently, the Internet seems to be the best and the most common way to gather such information. Recently, a deep-learning-based solution was proposed in the form of DeepAPI tool. Given English description of the desired functionality, sequence of Java function calls is generated. In this paper, we show the way to apply this approach to a different programming language (C# over Java) that has smaller open code base; we describe techniques used to achieve results close to the original, as well as techniques that failed to produce an impact. Finally, we release our dataset, code and trained model to facilitate further research.
Бесплатно
Applying the methods of system analysis to teaching assistants’ evaluation
Статья научная
This article presents the results of applying various methods of system analysis (CATWOE, Rich Picture, AHP, Fuzzy AHP) to evaluation of teaching assistants. The soft and hard methods were applied. Methods of system analysis are considered as an example at the Higher School of Economics (HSE) in program “Teaching assistant”. The article shows the process of interaction of teaching assistants with students and faculty in the form of Rich Picture. Selection and analysis of criteria for the evaluation of training assistants are carried out. Three groups of criteria were defined: professional skills, communicating skills, personal qualities. Each group has some subcriteria, which were defined in brainstorm. Its own method was determined, which immediately allow drop some assistants. In addition, the application of the methods AHP and Fuzzy AHP type-2 to evaluate teaching assistants is considered. The strengths and weaknesses of each method are revealed. It is also shown that, despite the power of the methods of system analysis, it is necessary to use common sense and logic. Do not rely only on the numbers obtained by the methods of system analysis. In the process of work, the best teaching assistant is selected, and the group of the best teaching assistants is defined.
Бесплатно
Approach to anti-pattern detection in service-oriented software systems
Статья научная
A service-based approach is a method to develop and integrate program products in a modular manner where each component is available through any net and has the possibility of being dynamically collaborated with other services of the system at run time. That approach is becoming widely adopted in industry of software engineering because it allows the implementation of distributed systems characterized by high quality. Quality attributes can be about the system (e.g., availability, modifiability), business-related aspects (e.g., time to market) or about the architecture (e.g., correctness, consistency). Maintaining quality-attributes on a high level is critical issue because service-based systems lack central control and authority, have limited end-to-end visibility of services, are subject to unpredictable usage scenarios and support dynamic system composition. The constant evolution in systems can easily deteriorate the overall architecture of the system and thus bad design choices, known as anti-patterns, may appear. These are the patterns to be avoided. If we study them and are able to recognize them, then we should be able to avoid them. Knowing bad practices is perhaps as valuable as knowing good practices. With this knowledge, we can re-factor the solution in case we are heading towards an anti-pattern. As with patterns, anti-pattern catalogues are also available. In case of continues evolution of systems, it is metric-based techniques that can be applied to obtain valuable, factual insights into how services work. Given the clear negative impact of anti-patterns, there is a clear and urgent need for techniques and tools to detect them. The article will focus on rules to recognize symptoms of anti-patterns in service-based environment, automated approaches to detection and applying metric-based techniques to this analysis.
Бесплатно
Buffer overflow detection via static analysis: expectations vs. reality
Статья научная
Over the last few decades buffer overflow remains one of the main sources of program errors and vulnerabilities. Among other solutions several static analysis techniques were developed to mitigate such program defects. We analyzed different approaches and tools that address this issue to discern common practices and types of detected errors. Also, we explored some popular sets of synthetic tests (Juliet Test Suite, Toyota ITC benchmark) and set of buggy code snippets extracted from real applications to define types of defects that a static analyzer is expected to uncover. Both sources are essential to understand the design goals of a production quality static analyzer. Test suites expose a set of features to support that is easy to understand, classify, and check. On the other hand, they don’t provide a real picture of a production code. Inspecting vulnerabilities is useful but provides an exploitation-biased sample. Besides, it does not include defects eliminated during the development process (probably with the help of some static analyzer). Our research has shown that interprocedural analysis, path-sensitivity and loop handling are essential. An analysis can really benefit from tracking affine relations between variables and modeling C-style strings as a very important case of buffers. Our goal is to use this knowledge to enhance our own buffer overrun detector. Now it can perform interprocedural context- and path-sensitive analysis to detect buffer overflow mainly for static and stack objects with approximately 65% true positive ratio. We think that promising directions are improving string manipulations handling and combining taint analysis with our approaches.
Бесплатно
Building modular real-time software from unified component model
Статья научная
Modern real-time operating systems are complex embedded product made by many vendors: OS vendor, board support package vendor, device driver developers, etc. These operating systems are designed to run on different hardware; the hardware often has limited memory. Embedded OS contains many features and drivers to support different hardware. Most of the drivers are not needed for correct OS execution on a specific board. OS is statically configured to select drivers and features for each board. Modularity of OS simplifies both configuration and development. Splitting OS to isolated modules with well-specified interfaces reduces developers’ needs to interact during joint development. The configurator, in turn, can easily compose isolated components without component developers. We use formal models to specify components and their composition. Formal model describes the behavior of components and their interaction. Usage of formal models has many benefits. Models contain enough information to generate source code in C language. Our model is executable; this allows configurator to quickly verify the correctness of component configurations. Moreover, model contains constraints on its parameters. These constraints are internal consistency or some external properties. Constraints are translated into asserts in generated source code. Therefore, we can check these constraints both at model simulation and at source code execution. This paper presents our approach to describe such models at Scala language. We successfully tested the approach in RTOS JetOS.
Бесплатно
Certified grammar transformation to Chomsky normal form in F
Статья научная
Certified programming allows to prove that the program meets its specification. The check of correctness of a program is performed at compile time, which guarantees that the program always runs as specified. Hence, there is no need to test certified programs to ensure they work correctly. There are numerous toolchains designed for certified programming, but F* is the only language that support both general-purpose programming and semi-automated proving. The latter means that F* infers proofs when it is possible and a user can specify more complex proofs if necessary. We work on the application of this technique to a grammarware research and development project YaccConstructor. We present a work in progress verified implementation of transformation of Context-free grammar to Chomsky normal form, that is making progress toward the certification of the entire project. Among other features, F* system allows to extract code in F# or OCaml languages from a program written in F*. YaccConstructor project is mostly written in F#, so this feature of F* is of particular importance because it allows to maintain compatibility between certified modules and those existing in the project which are not certified yet. We also discuss advantages and disadvantages of such approach and formulate topics for further research.
Бесплатно
Checking parameterized Promela models of cache coherence protocols
Статья научная
This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems.
Бесплатно
Configurable system call tracer in QEMU emulator
Статья научная
Sometimes programmers face the task of analyzing the work of a compiled program. To do this, there are many different tools for debugging and tracing written programs. One of these tools is the analysis of the application through system calls. With a detailed study of the mechanism of system calls, you can find a lot of nuances that you have to deal with when developing a program analyzer using system calls. This paper discusses the implementation of a tracer that allows you to analyze programs based on system calls. In addition, the paper describes the problems that I had to face in its design and development. Now there are a lot of different operating systems and for each operating system must be developed its own approach to implementing the debugger. The same problem arises with the architecture of the processor, under which the operating system is running. For each architecture, the analyzer must change its behavior and adjust to it. As a solution to this problem, the paper proposes to describe the operating system model, which we analyze. The model description is a configuration file that can be changed depending on the needs of the operating systems. When a system call is detected the plugin collects the information downloaded from the configuration file. In a configuration file, arguments are expressions, so we need to implement a parser that needs to recognize input expressions and calculate their values. After calculating the values of all expressions, the tracer formalizes the collected data and outputs it to the log file.
Бесплатно
Статья научная
The paper proposes some approaches to functional verification of microprocessor communication controllers based on developing layered UVM (Universal Verification Methodology) test systems. In modern microprocessor systems there are a lots of controllers operating with their own data types. Communication controllers support transferring and transformation data between microprocessor units. Such transformation must be carried out quickly and without data corruption for the correct functioning of the whole system. Communication controllers could carry additional functions such transmission values of copies of the system registers, address translation and others. Brief overview of verification tools and benefits of application standalone simulation based verification for checking the correctness of communication subsystems are marked out in the paper. We present the approaches of construction a standalone UVM-based verification environment with checking module implemented in external functional reference model. We also propose some techniques for checking the correctness of communication subsystems: checking multiple-clock controllers using parametrized clock generator, supporting of credit exchange mechanisms. Presented approaches were used to verify the communication subsystem - Host-Bridge - of Sparc V9 eight-core microprocessor developed by MCST. The difficulties discovered in the process of test system developing and its resolutions are described in the paper. The results of using presented solutions for verification of communicating subsystem controllers and further plan of the test system enhancement are considered.
Бесплатно
Context-based model for concern markup of a source code
Статья научная
In this paper we describe our approach to representing concerns in an interface of an IDE to make navigation across crosscutting concerns faster and easier. Concerns are represented as a tree of an arbitrary structure, each node of the tree can be bound to a fragment of code. It allows one to quickly locate fragments in the source code and makes switching between software development tasks easier. We describe a model which specifies data structures used to store the information about these code fragments and algorithms used to find the code fragment in original or modified source code. The model describes the information about code fragments as a set of contexts. Another important feature of the model is language independency. The model supports different programming, mark-up, DSL-languages and any structured text, such as a documentation. Main goal is to keep concern tree consistent with evolving source code. Search algorithm is designed to work with a modified source code, where the code fragment may change. The model is implemented as a tool, which supports different programming languages and integrates into different editors and integrated development environments. Source code analysis is performed by a set of lightweight parsers. In case of significant changes if the code fragment may be not found automatically the tool helps a programmer to find one by suggesting possible places in the source code based on the stored information.
Бесплатно
Cryptographic stack machine notation one
Статья научная
A worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic stack machine. The paper presents the syntax and semantics of CMN.1 and the principles of implementation of the CMN.1-based executable protocol specification language. The core language library (the engine) performs all the message processing, whereas a specification should only provide the declarative definitions of the messages. If an outcoming message must be formed, the engine takes the CMN.1 definition as input and produces the binary data in consistency with it. When an incoming message is received, the engine verifies the binary data with respect to the given CMN.1 definition memorizing all the information needed in the further actions. The verification is complete: the engine decrypts the ciphertexts, checks the message authentication codes and signatures, etc. Currently, the author's proof-of-concept implementation of the language (embedded in Haskell) can translate a CMN.1-based specifications both to the interoperable implementations and to the programs for the ProVerif protocol analyzer. The excerpts from the CMN.1-based TLS protocol specification and corresponding automatically generated ProVerif program are provided as an illustration.
Бесплатно
Design and architecture of real-time operating system
Статья научная
Modern airliners such as Airbus A320, Boeing 787, and Russian MS-21 use so called Integrated Modular Avionics (IMA) architecture for airborne systems. This architecture is based on interconnection of devices and on-board computers by means of uniform real-time network. It allows significant reduction of cable usage, thus leading to reducing of takeoff weight of and airplane. IMA separates functions of collecting information (sensors), action (actuators), and avionics logic implemented by applied avionics software in on-board computers. International standard ARINC 653 defines constraints on the underlying real-time operation system and programming interfaces between operating system and associated applications. The standard regulates space and time partitioning of applied IMA-related tasks. Most existing operating systems with ARINC 653 support are commercial and proprietary software. In this paper, we present JetOS, an open source real-time operating system with complete support of ARINC 653 part 1 rev 3. JetOS originates from the open source project POK, created by French researchers. At that time POK was the only one open source OS with at least partial support for ARINC 653. Despite this, POK was not feasible for practical usage: POK failed to meet a number of fundamental requirements and was executable in emulator only. During JetOS development POK code was significantly redesigned. The paper discusses disadvantages of POK and shows how we solved those problems and what changes we have made in POK kernel and individual subsystems. In particular we fully rewrote real-time scheduler, network stack and memory management. Also we have added some new features to the OS. One of the most important features is system partitions. System partition is a specialized application with extended capabilities, such as access to hardware (network card, PCI controller etc.) Introduction of system partitions allowed us moving large subsystems out of the kernel and limiting the kernel to the minimal functionality: context switching, scheduling and message pass. In particular, we have moved network subsystem to system partition. This moving reduces kernel size and potentially reduces probability on having bug in kernel and simplifies verification process.
Бесплатно
Designing variability models for software, operating systems and their families
Статья научная
The complexity of existing Legacy systems and the difficulty of amending it led to the development of the new concept of variability of systems specified by a model of the characteristics of FM (Feature Model). In the paper, we discuss the approaches to formal definition of FM and creating on its basis variants of program systems (PS), operating systems (OS) and families of program systems (FPS) for PS and OS. We give methods of manufacturing of PS in the Product Family/Product Lines, the conveyor of K.Czarnecki for assembling of artifacts in the space of problems and solutions, logical-mathematical modeling of PS from the functional and interface objects by Object-Components Method (OCM), extraction of the functional elements from OS kernel to FM for the generation of new variants of the OS. We discuss approaches for formalization of variability of legacy and new PS and their FPS. The new concept of management of variability systems with help OCM is defined. The approach to verify models of the FM, PS, FPS and OS and to configuration of functional and interface objects for obtaining the variants of the resulting product are proposed. We elaborate the characteristics for the testing process of variants of the PS, OS and FPS.
Бесплатно
Developing a debugger for real-time operating system
Статья научная
In this paper, we report on the work in progress on the debugger project for real-time operating system JetOS for civil airborne systems. It is designed to work within Integrated Modular Avionics (IMA) architecture and implements ARINC 653 API specification. This operating system is being developed in the Institute for System Programming of the Russian Academy of Sciences and next step in developing this system is to create a tool to debug user-space applications on it. We also discuss the major requirements to such a debugger and show the difference between it and typical debugger, used by desktop developers. Moreover, we review a number of debuggers for various embedded systems and study their functionality. Finally, we present our solution that works both in emulator QEMU, which we use to emulate environment for our system, and on the target hardware. The presented debugger is based on GDB debugging framework but contains a number of extensions specific for debugging embedded applications. However, the implementation of the debugger is not complete yet and there is a number of features that can improve debugger usability, but it is already more functional than common GDB debugger for QEMU and, in contrast to other systems and their debuggers, where developers can use some functions to debug applications, but not all we need, our debugger meets the majority of our requirements and restrictions.
Бесплатно
