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

Journal of Computing Sciences in Colleges 2014年第1期30卷

作者： John Meinke Kelvin Sung Michael Panitz UMUC Europe University of Washington Bothell Software Programming Cascadia Community College

The Game-Themed CS1/2 project aims at producing game-like education materials for CS1/2 students and faculty with no background in videogames or computer graphics. As part of this project, a set of APIs have been developed to support the building of engaging and fun casual videogames using only targeted programming concepts. Elaborate teaching modules have been developed based on these APIs that include example game-like programs demonstrating each concept, written documentation and video explanations. [1] The APIs, completely independent from each other, are each designed to support one video game and to target a specific programming concept, e.g., conditionals, loops, or arrays. In this way, it is possible to pick and choose relevant materials to integrate into one's existing classes. In this tutorial, we will introduce the APIs and teaching modules, lead participants in developing their own casual games based our APIs, present our approach and results of using the materials in our classes, and finally, discuss with the group interests and strategies in integrating the materials in their own classes.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Methodology for Model-based Development and Automated Verification of software for Aerospace Systemsd

A Methodology for Model-based Development and Automated Veri...

引用

IEEE Aerospace Conference

作者： Maertin, Lukas Schatalov, Maxim Hagner, Matthias Goltz, Ursula Maibaum, Olaf TU Braunschweig Inst Programming & React Syst D-38106 Braunschweig Germany German Aerosp Ctr Simulat & Software Technol D-38108 Braunschweig Germany

ISBN: (纸本)9781467318112

Today's software for aerospace systems typically is very complex. This is due to the increasing number of features as well as the high demand for safety, reliability, and quality. This complexity also leads to significant higher software development costs. To handle the software complexity, a structured development process is necessary. Additionally, compliance with relevant standards for quality assurance is a mandatory concern. To assure high software quality, techniques for verification are necessary. Besides traditional techniques like testing, automated verification techniques like model checking become more popular. The latter examine the whole state space and, consequently, result in a full test coverage. Nevertheless, despite the obvious advantages, this technique is rarely yet used for the development of aerospace systems. In this paper, we propose a tool-supported methodology for the development and formal verification of safety-critical software in the aerospace domain. The methodology relies on the V-Model and defines a comprehensive work flow for model-based software development as well as automated verification in compliance to the European standard series ECSS-E-ST-40C. Furthermore, our methodology supports the generation and deployment of code. For tool support we use the tool SCADE Suite (Esterel Technology), an integrated design environment that covers all the requirements for our methodology. The SCADE Suite is well established in avionics and defense, rail transportation, energy and heavy equipment industries. For evaluation purposes, we apply our approach to an up-to-date case study of the TET-1 satellite bus. In particular, the attitude and orbit control software is considered. The behavioral models for the subsystem are developed, formally verified, and optimized.

关键词： aerospace computing aerospace safety attitude control control engineering computing formal verification

来源：评论

学校读者我要写书评

暂无评论

Xbase: Implementing domain-specific languages for Java

Xbase: Implementing domain-specific languages for Java

引用

作者： Efftinge, Sven Eysholdt, Moritz Köhnlein, Jan Zarnekow, Sebastian Hasselbring, Wilhelm Von Massow, Robert Hanus, Michael Itemis AG D-24143 Kiel Germany Software Engineering Group University of Kiel Germany Programming Languages and Compiler Construction Group University of Kiel Germany

Xtext is an open-source framework for implementing external, textual domain-specific languages (DSLs). So far, most DSLs implemented with Xtext and similar tools focus on structural aspects such as service specifications and entities. Because behavioral aspects are significantly more complicated to implement, they are often delegated to generalpurpose programming languages. This approach introduces complex integration patterns and the DSL's high level of abstraction is compromised. We present Xbase as part of Xtext, an expression language that can be reused via language inheritance in any DSL implementation based on Xtext. Xbase expressions provide both control structures and program expressions in a uniform way. Xbase is statically typed and tightly integrated with the Java type system. Languages extending Xbase inherit the syntax of a Java-like expression language as well as language infrastructure components, including a parser, an unparser, a linker, a compiler and an interpreter. Furthermore, the framework provides integration into the Eclipse IDE including debug and refactoring support. The application of Xbase is presented by means of a domain model language which serves as a tutorial example and by the implementation of the programming language Xtend. Xtend is a functional and object-oriented general purpose language for the Java Virtual Machine (JVM). It is built on top of Xbase which is the reusable expression language that is the foundation of Xtend. Copyright 2012 ACM.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Runtime Verification for Multicore SoC with High-Quality Trace Data

引用

ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS 2013年第2期18卷 1-26页

作者： Backasch, Rico Hochberger, Christian Weiss, Alexander Leucker, Martin Lasslop, Richard Tech Univ Dresden Inst Comp Engn Chair Embedded Syst Dresden Germany Tech Univ Darmstadt Chair Comp Syst Darmstadt Germany Accemic Kiefersfelden Germany Univ Lubeck Inst Software Engn & Programming Languages Lubeck Germany Steinbichler Optotech GmbH Wettenberg Germany

Multicore System-on-Chip (SoC) implementations of embedded systems are becoming very popular. In these systems it is possible to spread out computations over many cores. On one hand this leads to better energy efficiency if clock frequencies and core voltages are reduced. On the other hand this delivers very high performance to the software developer and thus enables complex software systems to be implemented. Unfortunately, debugging and validation of these systems becomes extremely difficult. Various technological approaches try to solve this dilemma. In this contribution we will show a new approach to observe multicore SoCs and make their internal operations visible to external analysis tools. Also, we show that runtime verification can be employed to analyze and validate these internal operations while the system operates in its normal environment. The combination of these two approaches delivers unprecedented options to the developer to understand and verify system behavior even in complex multicore SoCs.

关键词： Design Algorithms Performance Multicore SoC embedded system runtime verification synchronisation trace data test driven development

来源：评论

学校读者我要写书评

暂无评论

Dynamic verification of hybrid systems

Dynamic verification of hybrid systems

引用

Tools & Methods of Program Analysis (TMPA)

作者： Nikolay Pakulin Department of Software Engineeing Institute for System Programming of RAS Moscow Russia

In the recent decade we face aggressive replacement of analog control loops with digital ones. Even for critical systems there are ongoing projects for digital control: “Smart Grids” in power industry, “Integrated Modular Avionics” in aerospace, “Smart Fabrics” in manufacturing, etc. Introduction of large scale digital control channels raises the risks of faults that might result in heavy losses. Those risks call for new methods of analysis and verification, including modeling hybrid systems and model-based verification. The paper overviews a number of existing approaches to verification of hybrid systems and introduces architecture of a test bed for dynamic verification of models of hybrid systems.

关键词： Numerical models Mathematical model Testing Automata Analytical models Atmospheric modeling software packages

来源：评论

学校读者我要写书评

暂无评论

The functional programming language R and the paradigm of dynamic scientific programming (Position paper)

The functional programming language R and the paradigm of dy...

引用

13th Symposium on Trends in Functional programming, TFP 2012

作者： Widemann, Baltasar Trancón Y. Bolz, Carl Friedrich Grelck, Clemens Ecological Modelling and Computer Science Universität Bayreuth Germany Software Engineering and Programming Languages Heinrich-Heine-Universität Düsseldorf Germany Computer Systems Architecture Universiteit Van Amsterdam Netherlands

ISBN: (纸本)9783642404467

R is an environment and functional programming language for statistical data analysis and visualization. Largely unknown to the functional programming community, it is popular and influential in many empirical sciences. Due to its integrated combination of dynamic and reflective scripting on one hand, and array-based numerical computation on the other, R poses unique and challenging implementation problems, at odds with the conservative language technology employed by its developers. We discuss the background of R in historical context, highlight some of the more problematic language features, and discuss the potential for the effective use of state-of-the-art language technology in a future, safe and efficient implementation. © 2013 Springer-Verlag.

关键词： Data visualization

来源：评论

学校读者我要写书评

暂无评论

Synthesis-based variability control: Correctness by construction

Synthesis-based variability control: Correctness by construc...

引用

10th International Symposium on Formal Methods for Components and Objects, FMCO 2011

作者： Lamprecht, Anna-Lena Margaria, Tiziana Schaefer, Ina Steffen, Bernhard Department for Service and Software Engineering University of Potsdam Germany Institut für Softwaretechnik und Fahrzeuginformatik Technische Universität Braunschweig Germany Department for Programming Systems Technical University Dortmund Germany

ISBN: (纸本)9783642358869

In this paper, we show the power of combining modern synthesis technology with a constraint-oriented approach to variability modeling. This combination guarantees the validity of all the required properties simply by construction: including a new property simply requires adding a corresponding constraint. The synthesis procedure will then automatically take care that all generated variants are property-conform. This fully declarative approach leads to a very agile variability modeling framework, where new product lines guaranteeing new properties can be defined ad hoc and are, due to our synthesis technology, immediately operational. As the underlying constraint language allows fully describing the intended solution space without imposing any overspecification, neither on the structure, nor on the artifacts, our approach may in particular be regarded as a step from the today typical settings with closed-world assumption to one with an open-world assumption. Impact and ease of this method are illustrated along a small case study running on our prototypical framework implementation. © 2013 Springer-Verlag Berlin Heidelberg.

关键词： Artificial intelligence

来源：评论

学校读者我要写书评

暂无评论

Patterns of cross-language linking in java frameworks

Patterns of cross-language linking in java frameworks

引用

IEEE Workshop on Program Comprehension

作者： Philip Mayer Andreas Schroeder Chair for Programming and Software Engineering Ludwig-Maximilians-Universität München Germany

ISBN: (纸本)9781467330909

The term Cross-Language Linking refers to the ability to specify, locate, navigate, and keep intact the connections between artifacts defined in different programming languages used for building one software application. Although understanding cross-language links and keeping them intact during development and maintenance activities is an important productivity issue, there has been little research on understanding the characteristics of such connections. We have thus built a theory from case studies, specifically, three theory-selected Java cross-language frameworks, each of which links artifacts written in the Java programming language to artifacts written in a declarative, framework-specific domain specific language. Our main contribution is to identify, from these experiences, common patterns of cross-language linking in the domain of Java frameworks with DSLs, which besides their informative nature can also be seen as requirements for designing and building a linking language and tooling infrastructure.

关键词： Atmospheric modeling Springs Frequency control

来源：评论

学校读者我要写书评

暂无评论

A Methodology for Model-based Development and Automated Verification of software for Aerospace Systems

A Methodology for Model-based Development and Automated Veri...

引用

IEEE Aerospace Conference

作者： Lukas Martin Maxim Schatalov Matthias Hagner Ursula Goltz Olaf Maibaum Institute for Programming and Reactive Systems TU Braunschweig Simulation and Software Technology German Aerospace Center

ISBN: (纸本)9781467318129

关键词： aerospace systems computer software Quality assurance Workflow software design Verification state space safety-critical software computer programs test coverage Automation avionics Formal verification

来源：评论

学校读者我要写书评

暂无评论

Property-driven benchmark generation

Property-driven benchmark generation

引用

20th International Symposium on Model Checking software, SPIN 2013

作者： Steffen, Bernhard Isberner, Malte Naujokat, Stefan Margaria, Tiziana Geske, Maren Department of Programming Systems Dortmund University of Technology Dortmund D-44227 Germany Carnegie Mellon University Moffett Field CA United States Department of Service and Software Engineering Universität Potsdam Potsdam D-14482 Germany

ISBN: (纸本)9783642391750

We present a systematic approach to the automatic generation of platform-independent benchmarks of tailored complexity for evaluating verification tools for reactive systems. Key to this approach is a tool chain that essentially transforms a set of automatically generated LTL properties into source code for various formats, platforms, and competition scenarios via a sequence of property-preserving steps. These steps go through dedicated representations in terms of Büchi Automata, Mealy machines, Decision Diagram Models, Code Models, and finally the source code of the chosen scenario. The required transformations comprise LTL synthesis, model checking, property-oriented expansion, path condition extraction, theorem proving, SAT solving, and code motion. This combination allows us to address different communities via a growing set of programming languages, tailored sets of programming constructs, different notions of observation, and the full variety of LTL properties-ranging from mere reachability over general safety properties to arbitrary liveness properties. The paper illustrates the whole tool chain along accompanying examples, emphasizes the current state of development, and sketches the envisioned potential and impact of our approach. © 2013 Springer-Verlag Berlin Heidelberg.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：