检索结果-内蒙古大学图书馆

20th Conference Scientific Services and Internet, SSI 2018

作者： Burdonov, I.B. Evtushenko, N.V. Kossatchev, A.S. Ivannikov Institute for System Programming Russian Academy of Sciences Russia

The paper is devoted to deriving tests with guaranteed fault coverage for Finite State Machines (FSM). FSMs and their compositions are widely used when deriving tests for various systems, including interactive services, and the synchronous composition describes the behavior of a multi modular system when all the channels are active at each time instance. Without loss of generality, we assume that an output port of each FSM component is connected with at most one input port of another FSM component and propose a simplified approach for deriving the synchronous composition of deterministic complete FSMs using well known operators over FSMs. We also extend the sufficient conditions for checking the closure of the synchronous composition operator with respect to deterministic complete FSMs showing that for the operator closure it is sufficient that each composition cycle contains a Moore pair, i.e., a pair of some component FSM such that outputs do not significantly depend on inputs (Moore condition). If a system under test has the same structure as the reference composition and faults of component FSMs do not break the Moore condition, then a transition tour of the composed FSM is a good quality test when component states can be observed (testing with open state). We also propose how to derive a test with guaranteed fault coverage for a component FSM of our interest when states cannot be observed under the condition that input and output ports of a component under test can still be observed. © 2018 CEUR-WS. All rights reserved.

关键词： Testing

来源：评论

学校读者我要写书评

暂无评论

Quasi-Hydrodynamic Approach for Simulating Internal Wave Attractors

引用

Mathematical Models and Computer Simulations 2022年第4期14卷 547-558页

作者： Ryazanov, D.A. Ivannikov Institute of System Programming Russian Academy of Sciences Moscow Russian Federation

Abstract: On the example of the problem of modeling wave attractors in a stratified fluid, the advantages of the quasi-hydrodynamic (QHDFoam) algorithm over the classical algorithm of operator splitting (PISO) are demonstrated. Both algorithms are implemented by the finite volume method based on the OpenFOAM open source software package. It is shown that the application of the PISO algorithm does not reproduce the dynamics of multiple reflection and focusing of internal waves in a stratified fluid during the interaction with the boundaries of the computational domain. The QHDFoam algorithm based on solving the regularized Navier–Stokes equations gives results close to the data of the high-order spectral-element method, the data of which are considered as the reference in this study. © 2022, Pleiades Publishing, Ltd.

关键词： internal waves Nek5000 OpenFOAM QHDFoam wave attractors

来源：评论

学校读者我要写书评

暂无评论

ISE language: The ADL for efficient development of cross toolkits

ISE language: The ADL for efficient development of cross too...

引用

1st International Workshop on Model Based Architecting and Construction of Embedded systems, ACES-MB 2008 - Held as Part of the 2008 11th International Conference on Model Driven Engineering Languages and systems, MoDELS 2008

作者： Pakulin, Nikolay Rubanov, Vladimir Institute for System Programming Russian Academy of Sciences Moscow Russia

Cross toolkits (assembler, linker, debugger, simulator, profiler) are widely used for software-hardware codesign;an early creation of cross toolkits is an important success factor for industrial embedded systems. At the hardware design stage systems are subject to significant design alterations including changes in the instruction set of target CPUs. This is a challenging issue for early cross toolkit development. In this paper, we present a new Architecture Description Language (ADL) called ISE language and an approach to early cross toolkit development to cope with hardware design changes. The paper introduces the MetaDSP framework that supports ISE-based construction of cross toolkits and gives brief overview of the MetaDSP applications to industrial projects that proves the industrial strength of the presented approach and tools.

关键词： Embedded systems

来源：评论

学校读者我要写书评

暂无评论

Using Lingvodoc platform for researching genetic and areal semantic shifts: the case of Ob-Ugric basic vocabulary

Using Lingvodoc platform for researching genetic and areal s...

引用

2022 Ivannikov Open Conference, ISPRAS 2022

作者： Normanskaya, Julia V. Institute of Linguistics Ras Ivannikov Institute for System Programming Ras Moscow Russia

ISBN: (纸本)9798350398533

Article analysis consists the list the significance of the main results that were obtained when analyzing the graph-phonetic features of the first Cyrillic books in the XIX century:*** first Cyrillic books allow us to see how the classification of dialects *** first Cyrillic books allow you to date the time of phonetic *** first Cyrillic books make it possible to verify the accuracy of transcription of extinct dialects completed by different *** first Cyrillic books made it possible to identify phenomena that persist in modern dialects and existed in the XIX century, but previously did not attract the systematic attention of *** first Cyrillic books make it possible to clarify the territory where speakers of some dialects had previously *** first Cyrillic books confirm the reconstruction of the *** books allow us to clarify the reconstruction of the *** first Cyrillic books allow us to establish who was the true creator of literary languages. © 2022 IEEE.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

The verification of tunnel methods of the Extensible Authentication Protocol (EAP) 20

The verification of tunnel methods of the Extensible Authent...

引用

20th Conference Scientific Services and Internet, SSI 2018

作者： Nikeshin, A.V. Shnitman, V.Z. Ivannikov Institute for System Programming Russian Academy of Sciences Russia

In modern networks one of the main mechanisms of information security is the establishing of a secure tunnel and transmitting data under the protection of that tunnel. The same mechanism is used in some authentication protocols. Extensible Authentication Protocol (EAP) provide an effective flexible authentication mechanism, that can be easily expanded with new authentication methods. A tunnel-based methods of EAP executes various EAP methods under the protection of the secure tunnel. There are several tunnel-based EAP methods: Protected EAP (PEAP), EAP Tunneled TLS Authenticated Protocol (EAP-TTLS), EAP Flexible Authentication via Secure Tunneling (EAP-FAST), Tunnel EAP (TEAP). They all use Transport Layer Security protocol (TLS) to establish the secure tunnel. This paper presents approachs and results of verification of some tunnel-based methods of EAP Protocol using UniTESK technology and our team developments in testing network protocols. UniTESK technology allows to automate the process of test construction and evaluate whether an implementation conforms to the specification. Additional methods allow to send incorrect packets in each meaningful states of the protocol. © 2018 CEUR-WS. All rights reserved.

关键词： Formal specification

来源：评论

学校读者我要写书评

暂无评论

BinSide: Static Analysis Framework for Defects Detection in Binary Code

BinSide: Static Analysis Framework for Defects Detection in ...

引用

2020 Ivannikov Memorial Workshop, IVMEM 2020

作者： Aslanyan, Hayk Arutunian, Mariam Keropyan, Grigor Kurmangaleev, Shamil Vardanyan, Vahagn Russian-Armenian University System Programming Department Yerevan Armenia Yerevan State University Mathematics and Mechanics Department Yerevan Armenia Programming of the Russian Academy of Sciences Ivannikov Institute for System System Programming Department Moscow Russia

ISBN: (纸本)9781728190884

Software developers make mistakes that can lead to failures of a software product. One approach to detect defects is static analysis: examine code without execution. Currently, various source code static analysis tools are widely used to detect defects. However, source code analysis is not enough. The reason for this is the use of third-party binary libraries, the unprovability of the correctness of all compiler optimizations. This paper introduces BinSide: binary static analysis framework for defects detection. It does interprocedural, context-sensitive and flow-sensitive analysis. The framework uses platform independent intermediate representation and provide opportunity to analyze various architectures binaries. The framework includes value analysis, reaching definition, taint analysis, freed memory analysis, constant folding, and constant propagation engines. It provides API (application programming interface) and can be used to develop new analyzers. Additionally, we used the API to develop checkers for classic buffer overflow, format string, command injection, double free and use after free defects detection. © 2020 IEEE.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Testing of Communicating systems: Proceedings of the IFIP TC6 11th International Workshop on Testing of Communicating systems (Iwtcs '98), August 31-September 2, 1998, Tomsk, Russia

Testing of Communicating Systems: Proceedings of the IFIP TC...

引用

1998年

作者： Alexandre A Petrenko Nina V Yevtushenko

来源：评论

学校读者我要写书评

暂无评论

Robust Resource Partitioning Approach for ARINC 653 RTOS

Robust Resource Partitioning Approach for ARINC 653 RTOS

引用

2023 Ivannikov ISPRAS Open Conference, ISPRAS 2023

作者： Cheptsov, Vitaly Khoroshilov, Alexey Ivannikov Institute for System Programming of the Russian Academy of Sciences Moscow Russia

ISBN: (纸本)9798350349993

Modern airborne operating systems implement the concept of robust time and resource partitioning imposed by the standards for aerospace and airborne-embedded software systems, such as ARINC 653. While these standards do provide a considerable amount of design choices in regards to resource partitioning on the architectural and API levels, such as isolated memory spaces between the application partitions, predefined resource configuration, and unidirectional ports with limited queue and message sizes for inter-partition communication, they do not specify how an operating system should implement them in software. Furthermore, they often tend to set the minimal level of the required guarantees, for example, in terms of memory permissions, and disregard the hardware state of the art, which presently can provide considerably stronger guarantees at no extra cost. In the paper we present an architecture of robust resource partitioning for ARINC 653 real-time operating systems based on completely static MMU configuration. The architecture was implemented on different types of airborne hardware, including platforms with TLB-based and page table-based MMU. Key benefits of the proposed approach include minimised run-time overhead and simpler verification of the memory subsystem. © 2023 IEEE.

关键词： Real time systems

来源：评论

学校读者我要写书评

暂无评论

A locking protocol for scheduling transactions on XML data

A locking protocol for scheduling transactions on XML data

引用

2nd Spring Colloquium for Young Researchers in Databases and Information systems, SYRCoDIS 2005

作者： Pleshachkov, Peter Chardin, Petr Institute for System Programming RAS Morocco Moscow State University Russia

In this paper we propose a new DataGuide-based locking protocol for isolation of concurrent XML transactions. The protocol adopts DataGuide structure for locking purposes. We extend the multigranularity locking protocol by adding node and logical locks on DataGuide. This allows to enhance concurrency of XML-specific transactions, thereby increasing the overall system performance.

关键词： XML

来源：评论

学校读者我要写书评

暂无评论

Model based tool chain for system design and system integration of IMA

Model based tool chain for system design and system integrat...

引用

DAta systems In Aerospace, DASIA 2012

作者： Khoroshilov, Alexey Koverninskiy, Igor Olshanskiy, Mikhail Petrenko, Alexander Ugnenko, Alexander Institute for System Programming of Russian Academy of Sciences Russia GosNIIAS Russia

The paper presents a model-based tool chain for system design and system integration of integrated modular avionics in civil aviation domain. It describes architecture of the tool chain, its current state, use cases s... 详细信息

ISBN: (纸本)9789290922650

关键词： systems analysis

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：