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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

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

详细简洁

排序：

A Lightweight Approach to the Concurrent Use and Integration of SysML and formal methods in Systems Design 22

A Lightweight Approach to the Concurrent Use and Integration...

引用

acm/ieee 25th international conference on Model Driven Engineering Languages and Systems (models)

作者： Thorburn, Robert Sassone, Vladimiro Fathabadi, Asieh Salehi Aniello, Leonardo Butler, Michael Dghaym, Dana Hoang, Thai Son Univ Southampton Southampton Hants England

ISBN: (纸本)9781450394673

Increased systems complexity and ubiquitous computing drive the need for improved systems design. Model-based systems engineering using general purpose languages such as SysML, is a well-established response to this challenge. However, for systems where correctness-by-construction is critical, formal methods are often also deployed. This is a significant undertaking often involving complete model translation. We address this problem by developing a novel requirements interchange system, presented as a SysML model library, to guide the concurrent use of SysML and formal models without requiring complete model translation.

关键词： SysML formal methods model library requirements engineering

来源：评论

学校读者我要写书评

暂无评论

LION Real-Time I/O Transfer Control for Massively Parallel Processor Arrays 21

LION Real-Time I/O Transfer Control for Massively Parallel P...

引用

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

作者： Walter, Dominik Teich, Juergen Friedrich Alexander Univ Erlangen Nurnberg Hardware Software Codesign Erlangen Germany

ISBN: (纸本)9781450391276

The performance of many accelerator architectures depends on the communication with external memory. During execution, new I/O data is continuously fetched forth and back to memory. This data exchange is very often performance-critical and a careful orchestration thus vital. To satisfy the I/O demand for accelerators of loop nests, it was shown that the individual reads and writes can be merged into larger blocks, which are subsequently transferred by a single DMA transfer. Furthermore, the order in which such DMA transfers must be issued, was shown to be reducible to a real-time task scheduling problem to be solved at run time. Rather than just concepts, we investigate in this paper efficient algorithms, data structures and their implementation in hardware of such a programmable Loop I/O Controller architecture called LION that only needs to be synthesized once for each processor array size and I/O buffer configuration, thus supporting a large class of processor arrays. Based on a proposed heap-based priority queue, LION is able to issue every 6 cycles a new DMA request to a memory bus. Even on a simple FPGA prototype running at just 200 MHz, this allows for more than 33 million DMA requests to be issued per second. Since the execution time of a typical DMA request is in general at least one order of magnitude longer, we can conclude that this rate is sufficient to fully utilize a given memory interface. Finally, we present implementations on FPGA and also 22nm FDX ASIC showing that the overall overhead of a LION typically amounts to less than 5% of an overall processor array design.

关键词： Massively Parallel Processor Arrays TCPA I/O Scheduling Data Transfers Priority QueueZ

来源：评论

学校读者我要写书评

暂无评论

Towards Automated Input Generation for Sketching Alloy models 10

Towards Automated Input Generation for Sketching Alloy Model...

引用

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

作者： Jovanovic, Ana Sullivan, Allison Univ Texas Arlington Arlington TX 76019 USA

ISBN: (纸本)9781450392877

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well suited for verifying system designs. While Alloy comes deployed in the Analyzer, an automated scenario-finding tool set, writing correct models remains a difficult and error-prone task. ASketch is a synthesis framework that helps users build their Alloy models. ASketch takes as an input a partial Alloy models with holes and an AUnit test suite. As output, ASketch returns a completed model that passes all tests. ASketch's initial evaluation reveals ASketch to be a promising approach to synthesize Alloy models. In this paper, we present and explore SketchGen(2), an approach that looks to broaden the adoption of ASketch by increasing the automation of the inputs needed for the sketching process. Experimental results show SketchGen(2) is effective at producing both expressions and test suites for synthesis.

关键词： Alloys

来源：评论

学校读者我要写书评

暂无评论

Towards an Extensible Architecture and Tool Support for Model-based Verification

Towards an Extensible Architecture and Tool Support for Mode...

引用

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

作者： Delgado, David Burgueno, Lola Camara, Javier Troya, Javier Univ Malaga Malaga Spain Univ Malaga ITIS Software Malaga Spain

ISBN: (纸本)9798350324983

Model-based software engineering (MBSE) brings models to the center of software and system design. models are powerful abstractions used to support all phases of the software development life cycle of complex software. As these models grow larger and their complexity increases, they need to be verified and validated to preserve their correctness. One possible way to do so is by means of the use of formal methods. However, the availability of MBSE tools with support for validation and verification is limited, and they usually require the cumbersome deployment of software burdened by dependencies, preventing the adoption of these tools. This paper presents a web-based architecture designed to support the definition of domain models and provide translation capabilities to different verification formalisms. As a proof of concept for our architecture, we have developed a tool prototype that is light-weight, runs in the browser and supports: (i) definition of domain models represented as class diagrams and (ii) partial translation of class diagrams into the Alloy specification language, enabling verification of structural domain properties. We show how we have used this tool to verify properties for the public bus management system in the city of Malaga, Spain.

关键词： Model-based software engineering verification web-based modeling tool structural analysis domain models Alloy

来源：评论

学校读者我要写书评

暂无评论

A Secure Insulin Infusion System using Verification Monitors 21

A Secure Insulin Infusion System using Verification Monitors

引用

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

作者： Panda, Abhinandan Pinisetty, Srinivas Roop, Partha IIT Bhubaneswar Bhubaneswar India Univ Auckland Auckland New Zealand

ISBN: (纸本)9781450391276

Wearable and implantable medical devices are being increasingly deployed for diagnosis, monitoring, and to provide therapy for critical medical conditions. Such medical devices are examples of safety-critical, cyber-physical systems. In this paper we focus on insulin infusion systems (IISs), which are used by diabetics to maintain safe blood glucose levels. These systems support wireless features introducing potential vulnerabilities. Although these devices go through rigorous safety certification processes, these are not able to mitigate security threats. Based on published literature, attackers can remotely command to inject an incorrect amount of insulin thereby posing threat to a patient's life. While prior work based on formal methods have been proposed to detect potential attack vectors using different forms of static analysis, these have limitations in preventing attacks at run-time. Also, as these devices are safety critical, it is not possible to apply security patches, when new types of attacks are detected, due to the need for recertification. This paper addresses these limitations by developing a formal framework for the detection of cyber-physical attacks on an IIS. First, we propose a wearable device that senses the familiar ECG to detect attacks. Thus, this device is separate from the insulin infusion system, ensuring no need for recertification of IISs. To facilitate the design of this device, we establish a correlation of ECG intervals and blood glucose levels using statistical analysis. This helps us in proposing a framework for security policy mining using the developed statistical analysis. This paves the way for the design of formal verification monitors for IISs for the first time. We perform performance evaluation of the verification monitor, which proves the technical feasibility for the design of wearable devices for attack detection of IISs. Our approach is amenable to the application of security patches, when new attack vectors are detecte

关键词： formal methods Runtime monitoring Medical devices ECG signal

来源：评论

学校读者我要写书评

暂无评论

A Refined Model of Ill-definedness in Project-Based Learning 22

A Refined Model of Ill-definedness in Project-Based Learning

引用

acm/ieee 25th international conference on Model Driven Engineering Languages and Systems (models)

作者： Rump, Arthur Zaytsev, Vadim Univ Twente Comp Sci Enschede Netherlands Univ Twente Formal Methods & Tools Enschede Netherlands

ISBN: (纸本)9781450394673

Project-based courses are crucial to gain practically relevant knowledge in modelling and programming education. However, they fall into the "ill-defined" domain: there are many possible solutions;the quality of a deliverable is subjective and not formally assessable;reaching the goals means designing new artefacts and analysing new information;and the problem cannot always be divided into independent tasks. In this paper, we refine the existing two-dimensional (verifiability and solution space) classification of ill-defined classes of problems, contemplate methods and approaches for assessment of projects, and apply the model to analyse two study units of two different computer science programmes.

关键词： learning objectives

来源：评论

学校读者我要写书评

暂无评论

Counting Bugs in Behavioural models using Counterexample Analysis 10

Counting Bugs in Behavioural Models using Counterexample Ana...

引用

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

作者： Faqrizal, Irman Salaun, Gwen Univ Grenoble Alpes CNRS INRIA LIGGrenoble INP F-38000 Grenoble France

ISBN: (纸本)9781450392877

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking automatically verifies that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, but this counterexample does not precisely identify the source of the bug. In this work, we propose some techniques for simplifying the debugging of these models. These techniques first extract from the whole behavioural model the part which does not satisfy the given property. In that model, we then detect specific states (called faulty states) where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. By using this model, we propose in this paper some techniques to count the number of bugs in the original specification. The core idea of the approach is to change the specification for some specific actions that may cause the property violation, and compare the model before and after modification to detect whether this potential bug is one real bug or not. Beyond introducing in details the solution, this paper also presents tool support and experiments.

关键词： Behavioural models Model Checking Debugging Counterexample Bug Counting

来源：评论

学校读者我要写书评

暂无评论

Proceedings - ieee/acm 10th international conference on formal methods in Software Engineering, formaliSE 2022

Proceedings - IEEE/ACM 10th International Conference on Form...

引用

10th ieee/acm international conference on formal methods in Software Engineering, formaliSE 2022

ISBN: (纸本)9781450392877

The proceedings contain 12 papers. The topics discussed include: C for yourself: comparison of front-end techniques for formal verification;counting bugs in behavioral models using counterexample analysis;test suite generation for Boolean conditions with equivalence class partitioning;automatic loop invariant generation for data dependence analysis;counterexample-guided inductive repair of reactive contracts;towards automated input generation for sketching alloy models;formal specifications investigated: a classification and analysis of annotations for deductive verifiers;formal modeling and verification of multi-robot interactive scenarios in service settings;automating cryptographic protocol language generation from structured specifications;and generating counterexamples in the form of unit tests from Hoare-style verification attempts.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Resolving Goal-Conflicts and Scaling Synthesis through Mode-Based Decomposition 24

Resolving Goal-Conflicts and Scaling Synthesis through Mode-...

引用

44th international conference on Software Engineering: Companion Proceedings

作者： Brizzio, Matias Univ Politecn Madrid IMDEA Software Inst Madrid Spain

ISBN: (纸本)9798400705021

Reactive synthesis, with its roots in the work of A. Church, presents a transformative approach for the formal methods community. It seeks to translate system behaviors expressed in Linear-Time Temporal Logic (LTL) into correct-by-construction models using synthesis tools. However, this approach faces substantial challenges. Among these challenges is the high computational complexity of LTL synthesis, which constrains its application to large-scale systems. Additionally, unrealizable specifications present a significant obstacle as they act as barriers, impeding the synthesis process. Furthermore, the presence of goal-conflicts within requirements introduces contradictions and ambiguity, further complicating the synthesis process. These issues collectively make synthesis demanding, often resulting in suboptimal or unviable systems. Our research is dedicated to establishing a robust framework that systematically addresses these challenges, effectively bridging the gap between high-level requirements and dependable system realization. We prioritize refining requirement precision and advancing scalable synthesis techniques, offering advanced tools and methodologies to practitioners and researchers.

关键词： Search-based Software Engineering formal methods Requirements Engineering Evolutionary Computation Reactive Synthesis

来源：评论

学校读者我要写书评

暂无评论

Go with the Flow: Software Engineers and Distractions 22

Go with the Flow: Software Engineers and Distractions

引用

acm/ieee 25th international conference on Model Driven Engineering Languages and Systems (models)

作者： Janssens, Sabine Zaytsev, Vadim StressLabo Loonbeek Belgium Univ Twente Formal Methods & Tools Enschede Netherlands

ISBN: (纸本)9781450394673

Ideally, software engineers work in the state of flow: performing challenging tasks like system modelling with a series of routine actions, incorporating immediate IDE feedback, experiencing time distortion and managing harmful interruptions when necessary. We hypothesise that the ability to maintain the state of flow and the skill to get back into flow faster after being interrupted, are essential skills for software engineers, and that developing these increases the capacity to become good software engineers if given sufficient guidance and education. In this position paper, we link flow to trance and contemplate how techniques from the world of sport psychology can be used to teach learners to become better at software design, modelling, programming and debugging, as well as suggesting a means to assess the potential future success of undergraduate study seekers.

关键词： Flow hypnosis trance induction modelling programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共31页 << < 1 2 3 4 5 6 7 8 9 10 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：