اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدAutomatic Verification of Message-Based Device Drivers
109
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We develop a practical solution to the problem of automatic verification of the interface between device drivers and the OS. Our solution relies on a combination of improved driver architecture and verification tools. It supports drivers written in C and can be implemented in any existing OS, which sets it apart from previous proposals for verification-friendly drivers. Our Linux-based evaluation shows that this methodology amplifies the power of existing verification tools in detecting driver bugs, making it possible to verify properties beyond the reach of traditional techniques.
قيم البحث
اقرأ أيضاً
Evolution behaves like a tinkerer (Francois Jacob, Science, 1977). Software systems provide a unique opportunity to understand biological processes using concepts from network theory. The Debian GNU/Linux operating system allows us to explore the evo
lution of a complex network in a novel way. The modular design detected during its growth is based on the reuse of existing code in order to minimize costs during programming. The increase of modularity experienced by the system over time has not counterbalanced the increase in incompatibilities between software packages within modules. This negative effect is far from being a failure of design. A random process of package installation shows that the higher the modularity the larger the fraction of packages working properly in a local computer. The decrease in the relative number of conflicts between packages from different modules avoids a failure in the functionality of one package spreading throughout the entire system. Some potential analogies with the evolutionary and ecological processes determining the structure of ecological networks of interacting species are discussed.
A new style of temporal debugging is proposed. The new URDB debugger can employ such techniques as temporal search for finding an underlying fault that is causing a bug. This improves on the standard iterative debugging style, which iteratively re-ex
ecutes a program under debugger control in the search for the underlying fault. URDB acts as a meta-debugger, with current support for four widely used debuggers: gdb, MATLAB, python, and perl. Support for a new debugger can be added in a few hours. Among its points of novelty are: (i) the first reversible debuggers for MATLAB, python, and perl; (ii) support for todays multi-core architectures; (iii) reversible debugging of multi-process and distributed computations; and (iv) temporal search on changes in program expressions. URDB gains its reversibility and temporal abilities through the fast checkpoint-restart capability of DMTCP (Distributed MultiThreaded CheckPointing). The recently enhanced DMTCP also adds ptrace support, enabling one to freeze, migrate, and replicate debugging sessions.
The development of many highly dynamic environments, like pervasive environments, introduces the possibility to use geographically close-related services. Dynamically integrating and unintegrating these services in running applications is a key chall
enge for this use. In this article, we classify service integration issues according to interfaces exported by services and internal combining techniques. We also propose a contextual integration service, IntegServ, and an interface, Integrable, for developing services.
In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, these specifications need to be formalized in the input languages of all
formal tools that should be applied to analyse the models at different development levels. In this paper we propose a unified approach for the computer-assisted formal specification of requirements and their fully automated translation into the specification languages of different verification tools. We consider a two-stage MBD scenario where first Simulink models are developed from which executable code is generated automatically. We (i) propose a specification language and a prototypical tool for the formal but still textual specification of requirements, (ii) show how these requirements can be translated automatically into the input languages of Simulink Design Verifier for verification of Simulink models and BTC EmbeddedValidator for source code verification, and (iii) show how our unified framework enables besides automated formal verification also the automated generation of test cases.
This thesis describes our ongoing work on Contrastive Predictive Coding (CPC) features for speaker verification. CPC is a recently proposed representation learning framework based on predictive coding and noise contrastive estimation. We focus on inc
orporating CPC features into the standard automatic speaker verification systems, and we present our methods, experiments, and analysis. This thesis also details necessary background knowledge in past and recent work on automatic speaker verification systems, conventional speech features, and the motivation and techniques behind CPC.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
