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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

301 篇 会议
8 篇 期刊文献

馆藏范围

309 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

150 篇 工学
- 130 篇 计算机科学与技术...
- 118 篇 软件工程
- 22 篇 电气工程
- 16 篇 机械工程
- 13 篇 建筑学
- 12 篇 控制科学与工程
- 7 篇 信息与通信工程
- 6 篇 电子科学与技术（可...
- 1 篇 仪器科学与技术
- 1 篇 航空宇航科学与技...
- 1 篇 生物医学工程（可授...
- 1 篇 生物工程
- 1 篇 安全科学与工程
19 篇 理学
- 14 篇 数学
- 3 篇 系统科学
- 2 篇 生物学
- 1 篇 物理学
- 1 篇 化学
- 1 篇 统计学（可授理学、...
13 篇 艺术学
- 13 篇 设计学（可授艺术学...
11 篇 管理学
- 8 篇 管理科学与工程(可...
- 3 篇 工商管理
- 2 篇 图书情报与档案管...

主题

40 篇 analytical model...
38 篇 computational mo...
31 篇 formal methods
25 篇 hardware
22 篇 software
16 篇 model checking
16 篇 state-space meth...
15 篇 semantics
15 篇 data models
14 篇 computer archite...
14 篇 mathematical mod...
13 篇 safety
13 篇 automata
12 篇 software enginee...
12 篇 clocks
12 篇 verification
12 篇 formal verificat...
11 篇 algorithm design...
11 篇 adaptation model...
10 篇 computer science

机构

3 篇 sri internationa...
3 篇 cyber-physical s...
3 篇 univ twente form...
3 篇 univ calif berke...
2 篇 johannes kepler ...
2 篇 sri int menlo pk...
2 篇 computer enginee...
2 篇 dfki gmbh cyber ...
2 篇 iit delhi
2 篇 berlin institute...
2 篇 agh university o...
2 篇 university of ca...
2 篇 johannes kepler ...
2 篇 department of el...
2 篇 univ twente ensc...
2 篇 department of co...
2 篇 eindhoven univ t...
2 篇 univ oxford dept...
2 篇 mit comp sci & a...
2 篇 software modelin...

作者

4 篇 schneider klaus
4 篇 zaytsev vadim
4 篇 teich juergen
3 篇 talpin jean-pier...
3 篇 nils przigoda
3 篇 robert wille
3 篇 rolf drechsler
3 篇 gupta rajesh
2 篇 ruchkin ivan
2 篇 t. basten
2 篇 umeno shinya
2 篇 lim hongping
2 篇 axel legay
2 篇 chao wang
2 篇 o. sarbishei
2 篇 hoe james c.
2 篇 nathan allen
2 篇 sanjiva prasad
2 篇 allison sullivan
2 篇 mitra sayan

语言

309 篇 英文

检索条件"任意字段=IEEE/ACM International Conference on Formal Methods and Models for Codesign"

共 309 条记录，以下是81-90 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

Verifying Absence of Hardware-Software Data Races using Counting Abstraction

Verifying Absence of Hardware-Software Data Races using Coun...

引用

acm and ieee international conference on formal methods and models for Co-Design (MEMOCODE)

作者： Tuba Yavuz University of Florida Gainesville FL USA

ISBN: (数字)9781728191485

ISBN: (纸本)9781728191492

Device drivers are critical components of operating systems. However, due to their interactions with the hardware and being embedded in complex programming models implemented by the operating system, ensuring reliability of device drivers remains to be a challenge. In this paper, we focus on the interaction of the driver with the device and present an approach for modeling this interaction and verifying absence of hardware-software data races. Specifically, we use the counting abstraction technique to abstract dynamic process creation in response to I/O acknowledgements sent by the device. We present the results of our approach on the modeling and verification of several Linux device driver models.

关键词： Servers Keyboards Device drivers Programming Performance evaluation Linux Data models

来源：评论

学校读者我要写书评

暂无评论

Security-Driven Metrics and models for Efficient Evaluation of Logic Encryption Schemes 19

Security-Driven Metrics and Models for Efficient Evaluation ...

引用

17th acm-ieee Inter- national conference on formal methods and models for System Design (MEMOCODE)

作者： Hu, Yinghua Menon, Vivek V. Schmidt, Andrew Monson, Joshua French, Matthew Nuzzo, Pierluigi Univ Southern Calif Dept Elect & Comp Engn Los Angeles CA 90007 USA Univ Southern Calif Inst Informat Sci Arlington VA USA

ISBN: (纸本)9781450369978

Research in logic encryption over the last decade has resulted in various techniques to prevent different security threats such as Trojan insertion, intellectual property leakage, and reverse engineering. However, there is little agreement on a uniform set of metrics and models to efficiently assess the achieved security level and the trade-offs between security and overhead. This paper addresses the above challenges by relying on a general logic encryption model that can encompass all the existing techniques, and a uniform set of metrics that can capture multiple, possibly conflicting, security concerns. We apply our modeling approach to four state-of-the-art encryption techniques, showing that it enables fast and accurate evaluation of design trade-offs, average prediction errors that are at least 2x smaller than previous approaches, and the evaluation of compound encryption methods.

关键词： Cryptography

来源：评论

学校读者我要写书评

暂无评论

Security Types for Synchronous Data Flow Systems

Security Types for Synchronous Data Flow Systems

引用

acm and ieee international conference on formal methods and models for Co-Design (MEMOCODE)

作者： Sanjiva Prasad R.Madhukar Yerraguntla Subodh Sharma IIT Delhi India

ISBN: (数字)9781728191485

ISBN: (纸本)9781728191492

Synchronous reactive data flow is a paradigm that provides a high-level abstract programming model for embedded and cyber-physical systems, including the locally synchronous components of IoT systems. Security in such systems is severely compromised due to low-level programming, ill-defined interfaces and inattention to security classification of data. By incorporating a Denning-style lattice-based secure information flow framework into a synchronous reactive data flow language, we provide a framework in which correct-and-secure-by-construction implementations for such systems can be specified and derived. In particular, we propose an extension of the Lustre programming framework with a security type system. We prove the soundness of our type system with respect to the co-inductive operational semantics of Lustre by showing that well-typed programs exhibit non-interference.

关键词： Security Mathematical model Clocks Semantics Programming Lattices Data models

来源：评论

学校读者我要写书评

暂无评论

Lightweight formal Method for Robust Routing in Track-based Traffic Control Systems

Lightweight Formal Method for Robust Routing in Track-based ...

引用

acm and ieee international conference on formal methods and models for Co-Design (MEMOCODE)

作者： Maryam Bagheri Edward A. Lee Eunsuk Kang Marjan Sirjani Ehsan Khamespanah Ali Movaghar Sharif University of Technology Tehran Iran University of California at Berkeley Berkeley California USA Carnegie Mellon University Pittsburgh Pennsylvania USA Reykjavik University Mälardalen University Västeras Sweden University of Tehran Tehran Iran

ISBN: (数字)9781728191485

ISBN: (纸本)9781728191492

In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.

关键词： Mathematical model Metals Adaptation models Routing Control systems Computational modeling Analytical models

来源：评论

学校读者我要写书评

暂无评论

formal Modeling and Verification of Rate Adaptive Pacemakers for Heart Failure

Formal Modeling and Verification of Rate Adaptive Pacemakers...

引用

acm and ieee international conference on formal methods and models for Co-Design (MEMOCODE)

作者： Moon Soo Kim Weiwei Ai Partha S Roop Nathan Allen Rohit Ramchandra Julian Paton University of Auckland Auckland New Zealand Faculty of Medical and Health Sciences University of Auckland Auckland New Zealand

ISBN: (数字)9781728191485

ISBN: (纸本)9781728191492

Cardiovascular Implantable Electronic Devices (CIEDs) are routinely implanted to treat various types of arrhythmia. However, conventional pacing algorithms may not be able to provide optimal treatment for the patients with Heart Failure (HF) and evidence suggests negative outcomes. In this paper, we introduce a formal pacemaker model that can restore heart-lung synchronization, which may bring therapeutic benefits to the patient with chronic HF. We use valued Synchronous Discrete Timed Automata (SDTA) to describe the timing requirements of the device, which is then translated into Promela for formal verification through a set of rules which are defined to maintain the synchronous semantics. The safety-critical properties are then verified using the model checker SPIN. We show that the SDTA model can be verified more efficiently than conventional approaches with pure Timed Automata (TA). Animal test results show that the pacing rates are synchronized with the respiratory cycles. In particular, the functional safety is ensured under various respiratory conditions. This work yields, for the first time, a formal model of pacing device to reinstate heart rate variability for HF patients.

关键词： Pacemakers Heart Automata Clocks Adaptation models Synchronization Semantics

来源：评论

学校读者我要写书评

暂无评论

Semantic source code models using identifier embeddings 16

Semantic source code models using identifier embeddings

引用

16th ieee/acm international conference on Mining Software Repositories, MSR 2019

作者： Efstathiou, Vasiliki Spinellis, Diomidis Athens University of Economics and Business Greece

ISBN: (纸本)9781728134123

The emergence of online open source repositories in the recent years has led to an explosion in the volume of openly available source code, coupled with metadata that relate to a variety of software development activities. As an effect, in line with recent advances in machine learning research, software maintenance activities are switching from symbolic formal methods to data-driven methods. In this context, the rich semantics hidden in source code identifiers provide opportunities for building semantic representations of code which can assist tasks of code search and reuse. To this end, we deliver in the form of pretrained vector space models, distributed code representations for six popular programming languages, namely, Java, Python, PHP, C, C++, and C#. The models are produced using fastText, a state-of-the-art library for learning word representations. Each model is trained on data from a single programming language;the code mined for producing all models amounts to over 13.000 repositories. We indicate dissimilarities between natural language and source code, as well as variations in coding conventions in between the different programming languages we processed. We describe how these heterogeneities guided the data preprocessing decisions we took and the selection of the training parameters in the released models. Finally, we propose potential applications of the models and discuss limitations of the models. © 2019 ieee.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Securing Smart Contracts in Blockchain 34

Securing Smart Contracts in Blockchain

引用

34th ieee/acm international conference on Automated Software Engineering (ASE)

作者： Kongmanee, Jaturong Kijsanayothin, Phongphun Hewett, Rattikorn Texas Tech Univ Comp Sci Lubbock TX 79409 USA Naresuan Univ Elect & Comp Engn Phitsanulok Thailand

ISBN: (纸本)9781728141367

Blockchain is an emerging technology that underlies creation and exchange of the digital assets, including cryptocurrency such as Bitcoin and Ether, without the need for a central authority. It provides a public ledger for recording sequence of transactions in blocks that are linked as a chain. Smart contracts are computer programs governing participant agreements that are automatically enforced by consensus protocols in the blockchain. Together, blockchain and smart contracts revolutionize efficient transaction stores, services and workflows that work even among distrusting participants and without a trusted authority. Unfortunately, like most software, smart contracts are vulnerable as evidenced by a recent Decentralized Autonomous Organization (DAO) attack that lost cryptocurrency then-valued about $60 million. Correctness of executions alone is not sufficient to guarantee security of smart contracts. This paper addresses how we can apply model checking, a well-established formal verification technique, to help alleviate security issues in smart contract development. Most existing studies have focused on verification of smart contracts on a specific language and specific platform. Smart contracts may have hidden operational side effects that impact software behaviors. Thus, applying model checking to smart contracts is not necessarily straightforward. This paper presents a general technique for building the core functional models applicable for model checking to identify all possible executions that lead to security breaches. It also shows how resulting executions can be systematically analyzed to help identify security issues. The models are language and system independent in that they can represent any smart contract in any language or any platform. We illustrate and evaluate the technique with a widely used example of a smart contract in a financial system along with experimental results using a well-known model checker, NuSMV in various scenarios.

关键词： Smart Contract Blockchain Model Checking formal methods

来源：评论

学校读者我要写书评

暂无评论

Bayesian Statistical Model Checking for Continuous Stochastic Logic

Bayesian Statistical Model Checking for Continuous Stochasti...

引用

acm and ieee international conference on formal methods and models for Co-Design (MEMOCODE)

作者： Ratan Lal Weikang Duan Pavithra Prabhakar Kansas State University Manhattan Kansas USA

ISBN: (数字)9781728191485

ISBN: (纸本)9781728191492

In this paper, we propose a Bayesian approach to statistical model-checking (SMC) of discrete-time Markov chains with respect to continuous stochastic logic (CSL) specifications. While Bayesian approaches for simpler logic without nested probabilistic operators and Frequentist approaches for nested logic have been previously explored, the Bayesian approach for CSL consisting of nested probabilistic operators has not been addressed. The challenge in the nested case arises from the fact that unlike in probabilistic model-checking (PMC), where we obtain a definitive answer for the model-checking problem for the sub-formulas, instead, we only obtain a correct answer with a certain confidence, which needs to be factored into the recursive SMC algorithm. Here, we propose a Bayesian test based algorithm for CSL that has nested probabilistic operators. We have implemented our algorithm in a Python Toolbox. Our experimental evaluation shows that our Bayesian SMC approach performs better than both the frequentist SMC approach and PMC algorithms.

关键词： Probabilistic logic Bayes methods Markov processes Model checking Computational modeling Testing Approximation algorithms

来源：评论

学校读者我要写书评

暂无评论

UML Consistency Rules: a Case Study with Open-Source UML models

UML Consistency Rules: a Case Study with Open-Source UML Mod...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Damiano Torre Yvan Labiche Marcela Genero Maged Elaasar Claudio Menghi University of Luxembourg Luxembourg Carleton University Ottawa Canada University of Castilla-La Mancha Ciudad Real Spain

UML models are standard artifacts used by software engineers for designing software. As software is designed, different UML diagram types (e.g., class diagrams and sequence diagrams) are produced by software designers. Since the various UML diagram types describe different aspects of a software system, they are not independent but strongly depend on each other, hence they must be consistent. Inconsistencies cause faults in the final software systems. It is, therefore, paramount that they get detected, analyzed, and fixed. Consistency rules are a useful tool proposed in the literature to detect inconsistencies. They categorize constraints that help in identifying inconsistencies when violated. This case study aims at collecting and analyzing UML models with OCL consistency rules proposed in the literature and at promoting the development of a reference benchmark that can be reused by the (FM-)research community. We collected 33 UML consistency rules and 206 different UML diagrams contained in 34 open-source UML models presented in the literature. We propose an FM-based encoding of the consistency rules in OCL. This encoding allows analyzing whether the consistency rules are satisfied or violated within the 34 UML models. To assess the proposed benchmark, we analyzed how the UML models, consistency rules, diagram types contained in the benchmark help in assessing the consistency of UML models, and the consistency of diagrams across the different software development phases. Our results show that the considered UML models and consistency rules allowed identifying 2731 inconsistencies and that those inconsistencies refer to different software development phases. We concluded that the considered UML models and consistency rules could be considered as an initial benchmark that can be further extended by the research community.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Detecting Security Leaks in Hybrid Systems with Information Flow Analysis 19

Detecting Security Leaks in Hybrid Systems with Information ...

引用

17th acm-ieee Inter- national conference on formal methods and models for System Design (MEMOCODE)

作者： Luan Viet Nguyen Mohan, Gautam Weimer, James Sokolsky, Oleg Lee, Insup Alur, Rajeev Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781450369978

Information flow analysis is an effective way to check useful security properties, such as whether secret information can leak to adversaries. Despite being widely investigated in the realm of programming languages, information-flow-based security analysis has not been widely studied in the domain of cyber-physical systems (CPS). CPS provide interesting challenges to traditional type-based techniques, as they model mixed discrete-continuous behaviors and are usually expressed as a composition of state machines. In this paper, we propose a lightweight static analysis methodology that enables information security properties for CPS models. We introduce a set of security rules for hybrid automata that characterizes the property of non-interference. Based on those rules, we propose an algorithm that generates security constraints between each sub-component of hybrid automata, and then transforms these constraints into a directed dependency graph to search for non-interference violations. The proposed algorithm can be applied directly to parallel compositions of automata without resorting to model-flattening techniques. Our static checker works on hybrid systems modeled in Simulink/Stateflow format and decides whether or not the model satisfies non-interference given a user-provided security annotation for each variable. Moreover, our approach can also infer the security labels of variables, allowing a designer to verify the correctness of partial security annotations. We demonstrate the potential benefits of the proposed methodology on two case studies.

关键词： Information Flow Security Static Analysis Simulink/Stateflow models

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共31页 << < 5 6 7 8 9 10 11 12 13 14 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：