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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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 条记录，以下是111-120 订阅

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

详细简洁

排序：

Keynote talk II: Multiform logical time for Me/Mo-codesign

Keynote talk II: Multiform logical time for Me/Mo-codesign

引用

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

作者： Robert de Simone Inria Le Chesnay ÃŽle-de-France FR

ISBN: (纸本)9781509027927

There is now a consistent corpus of models and methods for software/hardware codesign (scope of MeMoCoDe). Still, while success is quite established at both ends of the spectrum (High-Level hardware Synthesis, and System Engineering), the adoption of such Software modeling approach inside mainstream Software Engineering communities could easily be improved. This is certainly so because some of the principles of application modeling do not exactly match, or elsewhere do not focus upon the same concerns, as traditional coding style. Putting forth the relevant important concepts for application modeling, while investigating their relevance to traditional engineering experience, is certainly a way to counter confusion. We view the notion of Multiform Logical Time as such a fundamental concept. In a first part of the talk we consider the premises of Multiform Logical Time in Embedded Design (its origin, its relevance at places of design flows); in a second part we introduce a small declarative language to express logical time properties, study its expressiveness and its associated analysis techniques.

关键词： Unified modeling language Embedded systems Semantics Parallel processing Algebra Model checking Collaboration

来源：评论

学校读者我要写书评

暂无评论

The Entity Labeling Pattern for Modeling Operating Systems Access Control 1

引用

12th international Joint conference on E-Business and Telecommunications (ICETE)

作者： Amthor, Peter Ilmenau Univ Technol POB 100565 D-98684 Ilmenau Germany

ISBN: (数字)9783319302225

ISBN: (纸本)9783319302225;9783319302218

To meet tightening security requirements, modern operating systems enforce mandatory access control based on formal security policies. To ensure the critical property of policy correctness, formal methods and models for both their specification and verification are used. The variety of these approaches reflects the diversity and heterogeneity of policy semantics, which makes policy engineering an intricate and error-prone process. Therefore, a common formal framework is needed that unifies both diverse access control systems on the one hand and diverse formal criteria of correctness on the other hand. This paper presents a step towards this goal. We propose to leverage core-based model engineering, a uniform approach to policy formalization, and refine it by adding typical semantic abstractions of contemporary policy-controlled operating systems. This results in a simple, yet highly flexible framework for formalization, specification and analysis of operating system security policies. We substantiate this claim by applying our method to the SELinux system and demonstrating the practical usage of the resulting model.

关键词： Security engineering Security policies Access control models Operating system security SELinux

来源：评论

学校读者我要写书评

暂无评论

Combining type-checking with model-checking for system verification 16

Combining type-checking with model-checking for system verif...

引用

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

作者： Zhiqiang Ren Hongwei Xi Computer Science Department Boston University Boston USA

ISBN: (纸本)9781509027910

We present ATS/PML, a modeling language with an expressive type system (supporting both dependent types and linear types), and argue that the types in ATS/PML can be of great help in detecting modeling errors at compile-time. On one hand, we introduce modeling primitives with well-designed types into ATS/PML to facilitate a synergic combination of type-checking with model-checking. On the other hand, we compile ATS/PML into Promela so that the SPIN modelchecker can be readily employed to perform checking on models constructed in ATS/PML.

关键词： Numerical models Semantics Computational modeling Programming Model checking Cognition

来源：评论

学校读者我要写书评

暂无评论

formal engineering frameworks in maritime domain awareness 16

Formal engineering frameworks in maritime domain awareness

引用

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

作者： Amir Yaghoubi Shahir Uwe Glässer Hamed Yaghoubi Shahir Mohammad A. Tayebi Hans Wehn Software Technology Lab Simon Fraser University Burnaby BC Canada Research & Development MDA Systems Ltd. Richmond BC Canada

ISBN: (纸本)9781509027910

Maritime domain awareness builds on services and systems for interactive situation analysis and decision support to assist marine authorities in their assessment of unfolding situations to determine a response to imminent danger or threats to critical infrastructure or sensitive ecosystems. We propose here a methodical and economically viable approach to systematically develop an advanced situation analysis and decision support framework using formal engineering methods that facilitate continuous design through experimental analysis and validation of situation analysis process models in a realistic operational context. Striving for scalable and extensible solutions, our framework seamlessly integrates qualitative and quantitative modeling methods. An exploratory executable prototype operating on maritime surveillance data has been developed and is being evaluated, gradually extending the feature scope.

关键词： Trajectory Observers Surveillance Analytical models Data models Time series analysis Artificial intelligence

来源：评论

学校读者我要写书评

暂无评论

Multiform logical time for me/mo-codesign 16

Multiform logical time for me/mo-codesign

引用

Proceedings of the 14th acm-ieee international conference on formal methods and models for System Design

作者： Robert de Simone INRIA France

ISBN: (纸本)9781509027910

There is now a consistent corpus of models and methods for software/hardware codesign (scope of MeMoCoDe). Still, while success is quite established at both ends of the spectrum (High-Level hardware Synthesis, and System Engineering), the adoption of such Software modeling approach inside mainstream Software Engineering communities could easily be improved. This is certainly so because some of the principles of application modeling do not exactly match, or elsewhere do not focus upon the same concerns, as traditional coding style. Putting forth the relevant important concepts for application modeling, while investigating their relevance to traditional engineering experience, is certainly a way to counter confusion. We view the notion of Multiform Logical Time as such a fundamental *** a first part of the talk we consider the premises of Multiform Logical Time in Embedded Design (its origin, its relevance at places of design flows); in a second part we introduce a small declarative language to express logical time properties, study its expressiveness and its associated analysis techniques.

关键词：

来源：评论

学校读者我要写书评

暂无评论

10th acm/ieee international conference on formal methods and models for codesign, MEMOCODE 2012

10th ACM/IEEE International Conference on Formal Methods and...

引用

10th acm/ieee international conference on formal methods and models for codesign, MEMOCODE 2012

ISBN: (纸本)9781467313124

The proceedings contain 15 papers. The topics discussed include: compositional performance verification of NoC designs;a correlation preserving performance analysis for stream processing systems;clearing the clutter: unified modeling and verification methodology for system level hardware design;improving design verifiability by early RTL coverability analysis;FAST: formal specification driven test harness generation;model-based diagnosis versus error explanation;preservation of LTL properties in desynchronized systems;polynomial datapath synthesis and optimization based on vanishing polynomial over Z2m and algebraic techniques;interactive verification of synchronous systems;MEMOCODE 2012 hardware/software codesign contest: DNA sequence aligner;Shepard: a fast exact match short read aligner fast CPU-based DNA sequence aligner models;and a general technique for deterministic model-cycle-level debugging.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A computer-algebraic approach to formal verification of data-centric low-level software 16

A computer-algebraic approach to formal verification of data...

引用

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

作者： Oliver Marx Carlos Villarraga Dominik Stoffel Wolfgang Kunz University of Kaiserslautern

ISBN: (纸本)9781509027910

methods of Computer Algebra have shown to be useful when formally verifying data-centric hardware designs. This has been demonstrated especially for cases where complex arithmetic computations are tightly coupled with the system's control structures at the bit level. As a consequence of current design trends, however, more and more functionality that was traditionally implemented in hardware is now shifted into the low-level software of the system. Not only control functions but also more and more arithmetic operations and other data-centric functions are involved in this shift. Motivated by this observation, it is the goal of our work to extend the scope of computer-algebraic methods from hardware to low-level software. The paper develops how hardware-dependent software can be modeled algebraically so that efficient proof procedures are possible. Our results show that also in low-level software a computer-algebraic approach can have substantial advantages over state-of-the-art SMT solving.

关键词： Software Computational modeling Hardware Computers Algebra Analytical models Market research

来源：评论

学校读者我要写书评

暂无评论

Towards integrating statistical model checking into property-based testing 16

Towards integrating statistical model checking into property...

引用

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

作者： Bernhard K. Aichernig Richard Schumi Institute of Software Technology Graz University of Technology Austria

ISBN: (纸本)9781509027910

In recent years statistical model checking (SMC) became increasingly popular, mainly because it does not suffer from one of the major problems that limits traditional model checking, the so called state-space-explosion problem. SMC solves this problem by simulating a stochastic model for finitely many executions. There exist a number of SMC tools, but they require the user to learn a specific modelling language and a particular (temporal) logic to express properties. In this paper we propose a more flexible application of SMC, where both the model and the properties can be defined in a programming language. The technique builds upon the well-known property-based testing approach. We use the programming language C# and its associated tool FsCheck to demonstrate our approach. A stochastic counter serves as illustrating example.

关键词： Mathematical model Testing Stochastic processes Object oriented modeling Automata Monte Carlo methods Power capacitors

来源：评论

学校读者我要写书评

暂无评论

Clocks vs. instants relations: Verifying CCSL time constraints in UML/MARTE models 16

Clocks vs. instants relations: Verifying CCSL time constrain...

引用

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

作者： Judith Peters Nils Przigoda Robert Wille Rolf Drechsler Department of Satellite Ground Systems OHB System AG Bremen Germany Cyber-Physical Systems DFKI GmbH Bremen Germany Institute of Computer Science University of Bremen Bremen Germany Institute for Integrated Circuits Linz Austria Cyber-Physical Systems DFKI GmbH 28359 Bremen Germany

ISBN: (纸本)9781509027910

The specification of non-functional requirements, e. g., on timing forms an essential part of modern system design. Modeling languages such as MARTE/CCSL provide dedicated description means enabling engineers to formally define the ticking of the clocks to be implemented in terms of clock constraints and the actually intended timing behavior in terms of instant relations. But thus far, instant relations have only been utilized in order to monitor the correct execution of the clock constraints. In this work, we propose a methodology which, for the first time, verifies clock constraints against the given instant relations. To this end, the timing behavior is represented in terms of an automaton followed by its verification through satisfiability solvers. A case study illustrates the application of the proposed methodology.

关键词： Clocks Timing Satellites Unified modeling language Monitoring Integrated circuit modeling Sensors

来源：评论

学校读者我要写书评

暂无评论

Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics 15

Process algebra semantics & reachability analysis for micro-...

引用

2015 acm/ieee international conference on formal methods and models for codesign (MEMOCODE)

作者： Wouda, Sanne Joosten, Sebastiaan J. C. Schmaltz, Julien Eindhoven Univ Technol Dept Math & Comp Sci NL-5600 MB Eindhoven Netherlands

ISBN: (纸本)9781509002375

We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of NUXMV. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

关键词： process algebra reachability analysis Semantics semiotics islands Communication Research Textile fabrics fabric Abstraction

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共31页 << < 8 9 10 11 12 13 14 15 16 17 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：