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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

详细简洁

排序：

Preprocessing is What You Need: Understanding and Predicting the Complexity of SAT-based Uniform Random Sampling

Preprocessing is What You Need: Understanding and Predicting...

引用

FME Workshop on formal methods in Software Engineering (formaliSE)

作者： Olivier Zeyen Maxime Cordy Gilles Perrouin Mathieu Acher University of Luxembourg SnT Luxembourg PReCISE/NaDI University of Namur Belgium Univ Rennes Inria CNRS IRISA France

ISBN: (数字)9798400705892

ISBN: (纸本)9798350353662

Despite its NP-completeness, the Boolean satisfiability problem gave birth to highly efficient tools that are able to find solutions to a Boolean formula and compute their number. Boolean formulae compactly encode huge, constrained search spaces for variability-intensive systems, e.g., the possible configurations of the Linux kernel. These search spaces are generally too big to explore exhaustively, leading most testing approaches to sample a few solutions before analysing them. A desirable property of such samples is uniformity: each solution should get the same selection probability. This property motivated the design of uniform random samplers, relying on SAT solvers and counters and achieving different tradeoffs between uniformity and scalability. Though we can observe their performance in practice, understanding the complexity these tools face and accurately predicting it is an under-explored problem. Indeed, structural metrics such as the number of variables and clauses involved in a formula poorly predict the sampling complexity. More elaborated ones, such as minimal independent support (MIS), are intractable to compute on large formulae. We provide an efficient parallel algorithm to compute a related metric, the number of equivalence classes, and demonstrate that this metric is highly correlated to time and memory usage of uniform random sampling and model counting tools. We explore the role of formula preprocessing on various metrics and show its positive influence on correlations. Relying on these correlations, we train an efficient classifier (F1-score 0.97) to predict whether uniformly sampling a given formula will exceed a specified budget. Our results allow us to characterise the similarities and differences between (uniform) sampling, solving and counting.

关键词： Measurement Correlation Scalability Memory management Predictive models Complexity theory Computational efficiency

来源：评论

学校读者我要写书评

暂无评论

Semantic Comparisons of Alloy models 20

Semantic Comparisons of Alloy Models

引用

23rd acm/ieee international conference on Model Driven Engineering Languages and Systems (models)

作者： Ringert, Jan Oliver Wali, Syed Waqee Univ Leicester Leicester Leics England

ISBN: (纸本)9781450370196

Alloy is a textual modeling language for structures and behaviors of software designs. The Alloy Analyzer provides various analyses making it a popular light-weight formal methods tool. While Alloy models can be analyzed, explored, and tested, there is little support for comparing different versions of Alloy models. We believe that these comparisons are crucial when trying to refactor, refine, or extend models. In this work we present an approach for the semantic comparisons of Alloy models. Our pair-wise comparisons include semantic model differencing and the checking of refactoring, refinement, and extension. We enable semantic comparisons of Alloy models by a translation of two versions into a single model that is able to simulate instances of either one or of the versions. Semantic differencing and instance computation require only a single analysis of the combined model in the Alloy Analyzer. We implemented our work and evaluated it using 654 Alloy models from different sources including version histories. Our evaluation examines the cost of semantic comparisons using the Alloy Analyzer in terms of running times and variable numbers over individual models.

关键词： Alloy Specification Differencing Semantics Evolution

来源：评论

学校读者我要写书评

暂无评论

A Contrastive Plan Explanation Framework for Hybrid System models 18

A Contrastive Plan Explanation Framework for Hybrid System M...

引用

18th acm-ieee international conference on formal methods and models for System Design (MEMOCODE)

作者： Sarwar, Mir Md Sajid Ray, Rajarshi Banerjee, Ansuman Indian Assoc Cultivat Sci Sch Math & Computat Sci Kolkata India Indian Stat Inst Adv Comp & Microelect Unit Kolkata India

ISBN: (纸本)9781728191485

In artificial intelligence planning, having an explanation of a plan given by a planner is often desirable. The ability to explain various aspects of a synthesized plan to an end-user not only brings in trust on the planner but also reveals insights of the planning domain and the planning process. Contrastive questions such as "Why action A instead of action B?" can be answered with a contrastive explanation that compares properties of the original plan containing A against the contrastive plan containing B. In this paper, we explore a set of contrastive questions that a user of a planning tool may raise and we propose a re-model and re-plan framework to provide explanations to such questions. Earlier work has reported this framework on planning instances for discrete problem domains described in the Planning Domain Definition Language (PDDL) and its variants. In this paper, we propose an extension for planning instances described by PDDL+ for hybrid systems which portray a mix of discrete-continuous dynamics. Specifically, given a mixed discrete continuous system model in PDDL+ and a plan describing the set of desirable actions on the same to achieve a destined goal, we present a framework that can integrate contrastive questions in PDDL+ and synthesize alternate plans. We present a detailed case study on our approach and propose a comparison metric to compare the original plan with the alternate ones.

关键词： Hybrid systems

来源：评论

学校读者我要写书评

暂无评论

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

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

引用

ieee/acm 8th international conference on formal methods in Software Engineering (formaliSE)

作者： Torre, Damiano Labiche, Yvan Genero, Marcela Elaasar, Maged Menghi, Claudio Univ Luxembourg Luxembourg Luxembourg Carleton Univ Ottawa ON Canada Univ Castilla La Mancha Ciudad Real Spain

ISBN: (纸本)9781450370714

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 thefi nal software systems. It is, therefore, paramount that they get detected, analyzed, andfi xed. 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.

关键词： Case Study UML consistency rules Benchmark OCL Open-source models Model Checking

来源：评论

学校读者我要写书评

暂无评论

Verification of Privacy- Enhanced Collaborations 8

Verification of Privacy- Enhanced Collaborations

引用

ieee/acm 8th international conference on formal methods in Software Engineering (formaliSE)

作者： Belluccini, Sara De Nicola, Rocco Dumas, Marlon Pullonen, Pille Re, Barbara Tiezzi, Francesco IMT Sch Adv Studies Lucca Italy Univ Tartu Tartu Estonia Cybernetica AS Tallinn Estonia Univ Camerino Camerino Italy

ISBN: (纸本)9781450370714

In a distributed scenario it is possible to find systems consisting of independent parties that collaboratively execute a business process, but cannot disclose a subset of the data used in this process to each other. Such systems can be modelled using the PE-BPMN notation: a privacy-enhanced extension of the BPMN process modeling notation. Given a PE-BPMN model, we address the problem of verifying that the content of certain data objects is not leaked to unauthorized parties. To this end, we formalise the semantics of PE-BPMN collaboration diagrams via a translation into process algebraic specifications. This formalisation enables us to apply model checking to detect unintended data leakages in a PE-BPMN model. We specifically consider data leakages in the context of secret sharing technology. The approach has been implemented on top of the mCRL2 toolset, and integrated into the Pleak toolset supporting privacy analysis of business processes. The proposal has been evaluated using real scenarios.

关键词： Privacy-Enhanced Collaboration models Model Checking Verification PE-BPMN mCRL2 Data Leakage

来源：评论

学校读者我要写书评

暂无评论

Validation Obligations: A Novel Approach to Check Compliance between Requirements and their formal Specification

Validation Obligations: A Novel Approach to Check Compliance...

引用

ieee/acm international conference on Software Engineering: New Ideas and Emerging Technologies Results Track (ICSE-NIER)

作者： Atif Mashkoor Michael Leuschel Alexander Egyed Johannes Kepler University Linz Austria Heinrich Heine University Dϋsseldorf Germany

ISBN: (纸本)9781665429740

Traditionally, practitioners use formal methods pre-dominately for one half of the quality-assurance process: verification (do we build the software right?). The other half - validation (do we build the right software?) - has been given comparatively little attention. While verification is the core of refinement-based formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus mistakes in requirementsor in their interpretation are caught too late: usually at the endof the development process. In this paper, we present a novelapproach to check compliance between requirements and theirformal refinement-based specification during the earlier stages ofdevelopment. Our proposed approach - "validation obligations"- is based on the simple idea that both verification and validationare an integral part of all refinement steps of a system.

关键词： Adaptation models Velocity control Prototypes Tools Software formal specifications Software engineering

来源：评论

学校读者我要写书评

暂无评论

2018 16th acm/ieee international conference on formal methods and models for System Design, MEMOCODE 2018

2018 16th ACM/IEEE International Conference on Formal Method...

引用

16th acm/ieee international conference on formal methods and models for System Design, MEMOCODE 2018

ISBN: (纸本)9781538661956

The proceedings contain 13 papers. The topics discussed include: run-time requirement enforcement for loop programs on processor arrays;security of pacemakers using runtime verification;software engineering techniques for cyber-physical systems;synchronous neural networks for cyber-physical systems;UCLID5: integrating modeling, verification, synthesis and learning;towards dependability metrics for neural networks;formal analysis and verification of DDS in ROS2;desynchronization: from macro-step to micro-step;and it's a matter of time: modeling and analysis of time dependent systems using scenario-aware dataflow.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Reachability Analysis for Hybrid Systems with Nonlinear Guard Sets 23

Reachability Analysis for Hybrid Systems with Nonlinear Guar...

引用

23rd acm international conference on Hybrid Systems - Computation and Control ((HSCC)) part of CPS-IoT Week

作者： Kochdumper, Niklas Althoff, Matthias Tech Univ Munich Munich Germany

ISBN: (纸本)9781450370189

Reachability analysis is one of the most important methods for formal verification of hybrid systems. The main difficulty for hybrid system reachability analysis is to calculate the intersection between reachable set and guard sets. While there exist several approaches for guard sets defined by hyperplanes or polytopes, only few methods are able to handle nonlinear guard sets. In this work we present a novel approach to tightly enclose the intersections of reachable sets with nonlinear guard sets. One major advantage of our method is its polynomial complexity with respect to the system dimension, which makes it applicable for high-dimensional systems. Furthermore, our approach can be combined with different reachability algorithms for continuous systems due to its modular design. We demonstrate the advantages of our novel approach compared to existing methods with numerical examples.

关键词： hybrid systems nonlinear level sets Taylor models polynomial zonotopes

来源：评论

学校读者我要写书评

暂无评论

Teaching Software Modelling in an Undergraduate Introduction to Software Engineering 22

Teaching Software Modelling in an Undergraduate Introduction...

引用

acm/ieee 22nd international conference on Model Driven Engineering Languages and Systems Companion (models-C)

作者： Westphal, Bernd Albert Ludwigs Univ Freiburg Dept Comp Sci Freiburg Germany

ISBN: (纸本)9781728151250

In this article we present our design of an (otherwise completely ordinary) undergraduate introduction to software engineering with an emphasis on contemporary software modelling. A distinguishing aspect of our course is that we aim at a comprehensive introduction of modelling in two regards. Firstly, we introduce proper sub-languages of common modelling languages like UML class diagrams (rather than sampling examples or covering as many building blocks as possible) with a complete formal abstract syntax and semantics (so to give exact meaning to all models from the sub-language). Secondly, we emphasise issues arising from software models in the context of software engineering, e.g., that (formal) analysis results needs proper interpretation wrt. the considered software. We discuss our objectives wrt. modelling in software engineering, and outline the content of the course and the narratives that we use to reach these objectives. Evaluation results from four seasons of teaching the course give no indication of over-straining students wrt. level or workload.

关键词： education teaching software modelling software engineering formal methods

来源：评论

学校读者我要写书评

暂无评论

Towards a formal Specification of Multi-Paradigm Modelling 22

Towards a Formal Specification of Multi-Paradigm Modelling

引用

acm/ieee 22nd international conference on Model Driven Engineering Languages and Systems Companion (models-C)

作者： Amrani, Moussa Blouin, Dominique Heinrich, Robert Rensink, Arend Vangheluwe, Hans Wortmann, Andreas Univ Namur NaDI Fac Sci Namur Belgium Inst Polytech Paris Telecom Paris LTCI Paris France KIT Inst Program Struct & Data Org Karlsruhe Germany Univ Twente Formal Methods & Tools Twente Netherlands Univ Antwerp Flanders Make Modelling Simulat & Design Lab Antwerp Belgium Rhein Westfal TH Aachen Software Engn Aachen Germany

ISBN: (纸本)9781728151250

The notion of a programming paradigm is used to classify programming languages and their accompanying workflows based on their salient features. Similarly, the notion of a modelling paradigm can be used to characterise the plethora of modelling approaches used to engineer complex Cyber-Physical Systems (CPS). Modelling paradigms encompass formalisms, abstractions, workflows and supporting tool(chain)s. A precise definition of this modelling paradigm notion is lacking however. Such a definition will increase insight, will allow for formal reasoning about the consistency of modelling frameworks and may serve as the basis for the construction of new modelling, simulation, verification, synthesis, ...environments to support design of CPS. We present a formal framework aimed at capturing the notion of modelling paradigm, as a first step towards a comprehensive formalisation of multi-paradigm modelling. Our formalisation is illustrated by CookieCAD, a simple Computer-Aided Design paradigm used in the development of cookie stencils.

关键词： Modeling formal specifications Computer Programming Languages Workflow Plethora Support Tool First Step

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：