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

12th acm/ieee international conference on methods and models for system design, memocode 2014

ISBN: (纸本)9781479953387

the proceedings contain 27 papers. the topics discussed include: an abstraction-refinement framework for priority-driven scheduling of static dataflow graphs;a new synthesis procedure for atomic rules containing multi-cycle function blocks;from clock-driven to data-driven models;optimized distribution of synchronous programs via a polychronous model;three-valued asynchronous distributed runtime verification;a multi-core version of FreeRTOS verified for datarace and deadlock freedom;a framework for high-assurance quasi-synchronous systems;structure-aware CNF obfuscation for privacy-preserving SAT solving;performance analysis of the disrupted static priority scheduling for AFDX;are interface theories equivalent to contract theories?;and an architecturally-integrated, systems-based hazard analysis for medical applications.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Scenario-based system design with colored Petri nets: an application to train control systems

引用

SOFTWARE AND systemS MODELING 2018年第1期17卷 295-317页

作者： Wu, Daohua Schnieder, Eckehard Beijing Jiaotong Univ Natl Res Ctr Railway Safety Assessment Shangyuancun 3 Beijing 100044 Peoples R China Tech Univ Carolo Wilhelmina Braunschweig Inst Traff Safety & Automat Engn Hermann Blenk Str 42 D-38108 Braunschweig Germany

For the goal of model-based system software development, this paper exploits the formalism of colored Petri nets (CPNs) to design complex systems based on scenarios. the specification of UML sequence diagrams which are easily understood by customers, requirement engineers and software developers are adopted to represent scenarios as specification models. A scenario is a partial description of the system behavior, describing how users, system components and the environment interact. thus scenarios need to be synthesized in order to obtain an overall system behavior. A large number of works (e.g., Whittle and Schumann in Proceedings of the 2000 international conference on software engineering, pp 314-323, 2000;Elkoutbi and Keller in Application and theory of Petri nets, 2000;Damas et al. in Proceedings of the 14th acm SIGSOFT international symposium on foundations of software engineering, pp 197-207, 2000;Uchitel et al. in ieee Trans Softw Eng 29(2):99-115, 2003) have investigated scenario synthesis providing approaches or algorithms. these synthesis approaches and algorithms result in either Petri net models (e.g., Elkoutbi and Keller 2000;Ameedeen and Bordbar in 12th international ieee enterprise distributed object computing conference (EDOC), pp 213-221, 2008) that are mainly suitable for scenario validation or other forms of behavior models (e.g., labeled transition systems in Damas et al. 2000;Uchitel et al. 2003 and statecharts in Kruger et al. in Distributed and parallel embedded systems, pp 61-71, 1999;Whittle et al. 2000) that may be regarded as design models. Petri nets are well known for describing distributed and concurrent complex systems. Furthermore, numerous techniques, e.g., simulation, testing, state space-based techniques, structural methods and model checking, are currently available for analyzing Petri net models. therefore, design models in the form of Petri nets, integrating all scenarios into a coherent whole and fitting for further detailed de

关键词： Scenario system design Modeling Verification Colored Petri nets Train control system

来源：评论

学校读者我要写书评

暂无评论

Guest editorial: Special issue on models and methodologies for system design

Guest editorial: Special issue on models and methodologies f...

引用

作者： Ienne, Paolo Talpin, Jean-Pierre

this special issue is based on innovative ideas presented and discussed during the 12th acm/ieee international conference on Formal methods and models for system design (memocode'14) held at EPFL in Lausanne, Switzerland, on October 19-21, 2014. Selected papers from the conference were invited for this special issue together with an open call soliciting novel contributions on the topics of this conference. Rigorous reviews of 12 submissions led to the selection of four articles for this special issue. In this editorial statement, we outline the premise and the context of this special issue, give a short introduction to the theme under consideration, and briefly introduce the articles selected.

关键词： systems analysis

来源：评论

学校读者我要写书评

暂无评论

memocode 2014 software design contest: Space Invaders emulator 14

MEMOCODE 2014 software design contest: Space Invaders emulat...

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Edwards, Stephen A. Patel, Hiren Department of Computer Science Columbia University New YorkNY United States Electrical and Computer Engineering University of Waterloo WaterlooON Canada

ISBN: (纸本)9781479953387

the memocode design contest for 2014 was centered around the emulation of the 1978 Taito video game Space Invaders. the challenge is to improve the speed of a cycle-accurate software emulator for the game. Contestants had a month toope improve the provided code, which already ran fairly well on the ARM-based Raspberry Pi platform. Entries were judged on how much faster their code ran and its quality. the winning groups used a variety of optimization techniques ranging from dynamic binary translation, data-structure restructuring, and improving instruction and data caching. © 2014 ieee.

关键词： Software design

来源：评论

学校读者我要写书评

暂无评论

memocode 2014 design contest: K-Nearest Neighbors with Mahalanobis distance metric 14

MEMOCODE 2014 design contest: K-Nearest Neighbors with Mahal...

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Milder, Peter Department of Electrical and Computer Engineering Stony Brook University Stony BrookNY11794-2350 United States

ISBN: (纸本)9781479953387

the memocode 2014 hardware/software codesign contest problem is k-Nearest Neighbor search using the Mahalanobis distance metric. Given a data set of points in multi-dimensional space, the goal is to find the k points that are nearest to any given point in that space (quantified with the given distance metric). Contestants were given one month to develop a system to perform the kNN search, aiming to maximize performance or cost-adjusted performance. the two winning teams, which have been invited to contribute papers describing their techniques, combined algorithmic and implementation optimizations. the pure-performance winners targeted the Convey HC-2ex hybrid FPGA/multicore system, while the winners for cost-adjusted performance targeted an Intel multicore. © 2014 ieee.

关键词： Nearest neighbor search

来源：评论

学校读者我要写书评

暂无评论

Assertion-based flow monitoring of systemC models 14

Assertion-based flow monitoring of SystemC models

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Dutta, Sonali Vardi, Moshe Y. Rice University United States Synopsis United States

ISBN: (纸本)9781479953387

systemC is the de facto standard system-modeling language for hardware-software systems. A concurrent and reactive hardware-software system performs different 'jobs' during its execution. Each such job begins with a set of input data, flows through different processes in the system, and finally produces a set of output data. We call such a job a flow, since it flows from one process to another. Flows are dynamic and concurrent;a flow can begin anytime during the simulation and the system can process multiple flows at the same time. We provide a library for explicitly implementing flows in a systemC model or annotating flows in an existing systemC model with minimal modification. We also provide an automated monitoring framework for monitoring properties of flows. Such properties capture the reactive nature of a system naturally and are intuitive to write. Our experimental results show that the framework adds minimal simulation runtime overhead. © 2014 ieee.

关键词： Modeling languages

来源：评论

学校读者我要写书评

暂无评论

Building faithful high-level models and performance evaluation of manycore embedded systems 14

Building faithful high-level models and performance evaluati...

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Nouri, Ayoub Bozga, Marius Molnos, Anca Legay, Axel Bensalem, Saddek Univ. Grenoble Alpes VERIMAG GrenobleF-38000 France CEA LETI Grenoble France INRIA IRISA Rennes France

ISBN: (纸本)9781479953387

Performance and functional correctness are key for successful design of modern embedded systems. Both aspects must be considered early in the design process to enable founded decision making towards final implementation. Nonetheless, building abstract system-level models that faithfully capture performance information along to functional behavior is a challenging task. In contrast to functional aspects, performance details are rarely available during early design phases and no clear method is known to characterize them. Moreover, once such system-level models are built they are inherently complex as they usually mix software models, hardware architecture constraints and environment abstractions. their analysis by using traditional performance evaluation methods is reaching the limits and the need for more scalable and accurate techniques is becoming urgent. In this paper, we introduce a systematic method for building stochastic abstract performance models using statistical inference and model calibration and we propose statistical model checking as performance evaluation technique upon the obtained models. We experimented our method on a real-life case study and we were able to verify different timing properties. © 2014 ieee.

关键词： Embedded systems

来源：评论

学校读者我要写书评

暂无评论

From clock-driven to data-driven models 14

From clock-driven to data-driven models

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Bai, Yu Schneider, Klaus Bhardwaj, Nikita Katti, Badarinath Shazadi, Tania University of Kaiserslautern Kaiserslautern67653 Germany

ISBN: (纸本)9781479953387

Clock/time-driven models are powerful abstractions of real-time systems, as e.g., provided by the synchronous models of computation which lend themselves well for simulation and verification. At every clock cycle, new inputs are read, computations are performed in zero-time, and results are immediately/synchronously communicated between components. However, such zero-time idealizations are not realistic since computation and communication finally takes time in implementations. For implementations, data-driven execution models have the advantage to impose no timing constraints other than arrival of input data, and thus, these models are perfectly suited for distributed or other kinds of asynchronous implementations. For this reason, modern model-based design flows consider the desynchronization of synchronous models for system synthesis which is possible for the subclass of endochronous systems only. While definitions of endochrony were considered for years, it is shown in this paper how to efficiently verify endochrony by SAT solving. Our procedure consists of two steps: In the first step, we introduce buffers to the interface of a clock-driven component, so that its inputs can arrive at different points of time. After this step, clocks of signals are viewed as 'instructions' telling the component which input values have to be consumed for the current *** call such components clock-scheduled. In the second step, we remove the clocks from the interface of the clock-scheduled components, so that the component may now become nondeterministic. We prove in this paper that a synchronous component is endochronous, if and only if the clock signals can be safely removed in this step without destroying determinism. Based on this result, we present a decision procedure based on symbolic system representations to check whether components are endochronous. Preliminary experimental results show the effectiveness of our method. © 2014 ieee.

关键词： Clocks

来源：评论

学校读者我要写书评

暂无评论

A framework for high-assurance quasi-synchronous systems 14

A framework for high-assurance quasi-synchronous systems

引用

12th acm/ieee international conference on methods and models for system design, memocode 2014

作者： Larrieu, Robin Shankar, Natarajan École Polytechnique Palaiseau France SRI International Menlo ParkCA United States

ISBN: (纸本)9781479953387

the design of a complex cyber-physical system is centered around one or more models of computation (MoCs). these models define the semantic framework within which a network of sensors, controllers, and actuators operate and interact with each other. In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating system (ROS). It consists of nodes that encapsulate computation and topic channels that are used for communicating between nodes. the nodes execute with a fixed period with possible jitter due to local clock drift and scheduling uncertainties, but are not otherwise synchronized. the channels are implemented through a mailbox semantics. In each execution step, a node reads its incoming mailboxes, applies a next-step operation to update its local state, and writes to all its outgoing mailboxes. the underlying transport mechanism implements the mailbox-to-mailbox data transfer with some bounded latency. Messages can be lost if a mailbox is over-written before it is read. We prove a number of basic theorems that are useful for designing robust high-assurance cyber-physical systems using this simple model of computation. We show that depending on the relative rates of the sender and receiver, there is a bound on the number of consecutive messages that can be lost. By increasing the mailbox queue size to a given bound, message loss can be eliminated. We demonstrate that there is a bound on the age of inputs that are used in any processing step. this in turn can be used to bound the end-to-end sense-control-actuate latency. We illustrate how these theorems are useful in designing and verifying a thermostat-based heating system. Our proofs have been mechanically verified using the Prototype Verification system (PVS). © 2014 ieee.

关键词： Cyber Physical system

来源：评论

学校读者我要写书评

暂无评论

Performance Comparison of ieee 802.11 DCF and EDCA for Beaconing in Vehicular Networks

Performance Comparison of IEEE 802.11 DCF and EDCA for Beaco...

引用

11th international conference on Quantitative Evaluation of systems (QEST)

作者： Heijenk, Geert van Eenennaam, Martijn Remke, Anne Univ Twente Design & Anal Commun Syst POB 217 NL-7500 AE Enschede Netherlands

ISBN: (纸本)9783319106960;9783319106953

For use in vehicular networks, ieee 802.11p has been standardized as the underlying wireless system. the 802.11 standard distinguishes two main methods of operation with respect to channel access, the Distributed Coordination Function (DCF) and the Enhanced Distributed Channel Access (EDCA), where the latter is the mandated method to be used in vehicular networks (in 802.11p). We present validated analytical models for both DCF and EDCA, and compare both methods in the context of beaconing. We will show that, surprisingly, DCF outperforms EDCA under assumptions that are realistic for beaconing in vehicular networks.

关键词： ieee Standards

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：