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

16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

作者： Ciobaca, Stefan Alexandru Ioan Cuza Univ Fac Comp Sci Iasi Romania

ISBN: (纸本)9781479984480

Two programs P and Q are partially equivalent if, when both terminate on the same input, they end up with equivalent outputs. Establishing partial equivalence is useful in, e.g., compiler verification, when P is the source program and Q is the target program, or in compiler optimisation, when P is the initial program and Q is the optimised program. A program R is partially correct if, when it terminates, it ends up in a "good" state. We show that, somewhat surprisingly, the problem of establishing partial equivalence can be reduced to the problem of showing partial correctness in an aggregated language, where programs R consist of pairs of programs < P, Q >. Our method is crucially based on the recently-introduced matching logic, which allows to faithfully define the operational semantics of any language. We show that we can construct the aggregated language mechanically, from the semantics of the initial languages. Furthermore, matching logic gives us for free a proof system for partial correctness for the resulting language. This proof system can then be used to prove partial equivalence.

关键词： optimising compilers program verification programming language semantics aggregated language compiler optimisation compiler verification matching logic operational language semantics partial correctness partial equivalence reduction proof system source program target program Cognition Cost accounting Optimization Production Program processors Reactive power semantics language semantics program equivalence relational logic proof systems object programs Source code programming language semantics Program processors semantics cost accounting program verification Reactive power Quality factor Cognition language semiotics relational logic accuracy class

来源：评论

学校读者我要写书评

暂无评论

A formal semantics of PLC programs in Coq

A formal semantics of PLC programs in Coq

引用

35th Annual IEEE International Computer Software and Applications Conference (COMPSAC)

作者： Ould Biha, Sidi INRIA FORMES Project Beijing Peoples R China

ISBN: (纸本)9780769544397

Programmable logic Controllers (PLC) are embedded systems that are widely used in industry. We propose a formal semantics of the Instruction List (IL) language, one of the five programing languages defined in the IEC 61131-3 standard for PLC programing. This semantics support a significant subset of the IL language that includes on-delay timers. We formalized this semantics in the proof assistant Coq and used it to prove some safety properties on an example of PLC program.

关键词： Coq Coq Delay IEC 61131-3 standard IEC standards Industries Instruction List PLC PLC programs Registers SSReflect Safety semantics Strontium embedded systems embedded systems formal semantics formal semantics instruction list language instruction sets programing languages programmable controllers programmable logic controllers programming language semantics proof assistant safety properties set theory subset theorem proving

来源：评论

学校读者我要写书评

暂无评论

Designing Dialects of Enterprise Modeling languages with the Profiling Technique 19

Designing Dialects of Enterprise Modeling Languages with the...

引用

19th IEEE International Enterprise Distributed Object Computing Conference (EDOC)

作者： Braun, Richard Esswein, Werner Tech Univ Dresden Chair Wirtschaftsinformat Esp Syst Dev D-01062 Dresden Germany

ISBN: (纸本)9781467392037

During the last years, several enterprise modeling languages became de-facto standards in their particular field of application. This dissemination increased the need for extending these languages in order to both specify concepts domain-specifically and integrate additional concepts. However, only the minority of enterprise modeling languages provides an extension mechanism and even those defining one, reveal some syntactical shortcomings. This issue can be also observed in the context of the well-known meta modeling language MOF and its correspondingly defined enterprise modeling languages like BPMN. This position paper therefore elaborates an adaptation of the profile mechanism from UML for generic extensions of meta models in the field of enterprise modeling. Therefore, the characteristics of profiling are abstracted to the meta meta model layer and comprehensively integrated within an framework for the integrated definition of meta models. The Stereotype concept is thereby applied to several parts of meta models including also aspects of the concrete syntax as well as semantics. The proposed framework serves as reference architecture for the derivation of meta modeling language specific implementations (e.g., within MOF).

关键词： Unified Modeling language business data processing corporate modelling program diagnostics programming language semantics BPMN MOF UML concept integration de-facto standards domain-specific concepts enterprise modeling languages dialect design meta modeling language specific implementations profile mechanism profiling characteristics profiling technique semantics stereotype concept syntax Adaptation models Context Context modeling Couplings semantics Syntactics Unified modeling language Abstract Syntax Extension Methods Meta Meta Modeling Meta Model Extensions Meta Object Facility Profiles UML semantics KAT8 gene programming language semantics analysis programme meta-models business data processing Context modeling syntax modelling languages semiotics Couplings Adaptation models

来源：评论

学校读者我要写书评

暂无评论

Domain-Specific languages and Diagram Customization for a Concurrent Engineering Environment

Domain-Specific Languages and Diagram Customization for a Co...

引用

IEEE Aerospace Conference

作者： Cole, Bjorn Dubos, Greg Banazadeh, Payam Reh, Jonathan Case, Kelley Wang, Yeou-Fang Jones, Susan Picha, Frank CALTECH Jet Prop Lab Pasadena CA 91109 USA

ISBN: (纸本)9781467318112

A major open question for advocates of Model-Based Systems Engineering (MBSE) is the question of how system and subsystem engineers will work together. The Systems Modeling language (SysML), like any language intended for a large audience, is in tension between the desires for simplicity and for expressiveness. In order to be more expressive, many specialized language elements may be introduced, which will unfortunately make a complete understanding of the language a more daunting task. While this may be acceptable for systems modelers, it will increase the challenge of including subsystem engineers in the modeling effort. One possible answer to this situation is the use of Domain-Specific languages (DSL), which are fully supported by the Unified Modeling language (UML). SysML is in fact a DSL for systems engineering. The expressive power of a DSL can be enhanced through the use of diagram customization. Various domains have already developed their own schematic vocabularies. Within the space engineering community, two excellent examples are the propulsion and telecommunication subsystems. A return to simple box-and-line diagrams (e. g., the SysML Internal Block Diagram) are in many ways a step backward. In order allow subsystem engineers to contribute directly to the model, it is necessary to make a system modeling tool at least approximate in accessibility to drawing tools like Microsoft PowerPoint and Visio. The challenge is made more extreme in a concurrent engineering environment, where designs must often be drafted in an hour or two. In the case of the Jet Propulsion Laboratory's Team X concurrent design team, a subsystem is specified using a combination of PowerPoint for drawing and Excel for calculation. A pilot has been undertaken in order to meld the drawing portion and the production of master equipment lists (MELs) via a SysML authoring tool, MagicDraw. Team X currently interacts with its customers in a process of sharing presentations. There are several

关键词： Unified Modeling language aerospace propulsion concurrent engineering programming language semantics systems engineering

来源：评论

学校读者我要写书评

暂无评论

VDM semantics of programming languages: combinators and monads

引用

FORMAL ASPECTS OF COMPUTING 2011年第2期23卷 221-238页

作者： Mosses, Peter D. Swansea Univ Dept Comp Sci Swansea W Glam Wales

The Vienna Development Method (VDM) was developed in the early 1970s as a variant of denotational semantics. VDM descriptions of programming languages differ from the original Scott-Strachey style by making extensive use of combinators which have a fixed operational interpretation. After recalling the main features of denotational semantics and the Scott-Strachey style, we examine the combinators of the VDM specification language, and relate them to monads, which were introduced more than 15 years later. We also suggest that use of further monadic combinators in VDM could be beneficial. Finally, we provide an overview of published VDM semantic descriptions of major programming languages.

关键词： programming language semantics Denotational semantics VDM Combinators Monads

来源：评论

学校读者我要写书评

暂无评论

A Generic Operational Metatheory for Algebraic Effects

A Generic Operational Metatheory for Algebraic Effects

引用

25th Annual IEEE Symposium on Logic in Computer Science (LICS)

作者： Johann, Patricia Simpson, Alex Voigtlaender, Janis Univ Strathclyde Glasgow G1 1XH Lanark Scotland Univ Edinburgh Sch Informat Edinburgh Midlothian Scotland Univ Bonn Inst Comp Sci D-53012 Bonn Germany

ISBN: (纸本)9780769541143

We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of algebraic effects, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power's structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive "basic preorder" on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.

关键词： algebra algebraic effects contextual preorder generic operational metatheory polymorphic programming language programming language semantics relational parametricity structural operational semantics syntactic analysis

来源：评论

学校读者我要写书评

暂无评论

RV-Match: Practical semantics-Based Program Analysis 28th

RV-Match: Practical Semantics-Based Program Analysis

引用

28th International Conference on Computer-Aided Verification (CAV)

作者： Guth, Dwight Hathhorn, Chris Saxena, Manasvi Rosu, Grigore Runtime Verificat Inc Urbana IL 61801 USA Univ Illinois Urbana IL 61801 USA Univ Missouri Columbia MO 65211 USA

ISBN: (纸本)9783319415284;9783319415277

We present RV-Match, a tool for checking C programs for undefined behavior and other common programmer mistakes. Our tool is extracted from the most complete formal semantics of the C11 language. Previous versions of this tool were used primarily for testing the correctness of the semantics, but we have improved it into a tool for doing practical analysis of real C programs. It beats many similar tools in its ability to catch a broad range of undesirable behaviors. We demonstrate this with comparisons based on a third-party benchmark.

关键词： C11 programming language semantics Undefined behavior Static analysis Abstract interpretation

来源：评论

学校读者我要写书评

暂无评论

A programming language Approach to Fault Tolerance for Fork-Join Parallelism

A Programming Language Approach to Fault Tolerance for Fork-...

引用

7th International Symposium on Theoretical Aspects of Software Engineering (TASE)

作者： Zengin, Mustafa Vafeiadis, Viktor Max Planck Inst Software Syst MPI SWS Saarbrucken Germany

ISBN: (纸本)9780769550534

When running big parallel computations on thousands of processors, the probability that an individual processor will fail during the execution cannot be ignored. Computations should be replicated, or else failures should be detected at run-time and failed subcomputations reexecuted. We follow the latter approach and propose a high-level operational semantics that detects computation failures, and allows failed computations to be restarted from the point of failure. We implement this high-level semantics with a lower-level operational semantics that provides a more accurate account of processor failures, and prove in Coq the correspondence between the high- and low-level semantics.

关键词： checkpointing fault tolerant computing parallel processing programming language semantics

来源：评论

学校读者我要写书评

暂无评论

VDM semantics of programming languages: combinators and monads

VDM semantics of programming languages: combinators and mona...

引用

Festschrift Symposium

作者： Mosses, Peter D. Swansea Univ Dept Comp Sci Swansea W Glam Wales

ISBN: (纸本)9783540752202

关键词： programming language semantics Denotational semantics VDM Combinators Monads

来源：评论

学校读者我要写书评

暂无评论

Assuring the Safety of On-Demand Medical Cyber-Physical Systems

Assuring the Safety of On-Demand Medical Cyber-Physical Syst...

引用

1st IEEE International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA)

作者： King, Andrew L. Feng, Lu Sokolsky, Oleg Lee, Insup Univ Penn Dept Comp & Informat Sci Philadelphia PA 19104 USA

ISBN: (纸本)9781479907984

We present an approach to establish safety of on-demand medical cyber-physical systems which are assembled to treat a patient in a specific clinical scenario. We treat such a system as a virtual medial device (VMD) and propose a model-based framework that includes a modeling language with formal semantics and a medical application platform (MAP) that provides the necessary deployment support for the VMD models.

关键词： medical computing patient treatment programming language semantics safety-critical software virtual reality

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：