Recently there has been considerable interest in programminglanguagesthat encode security policies in type declarations. Type-checking is used to determine whether a program enforces these policies. this approach en...
详细信息
ISBN:
(纸本)3540423141
Recently there has been considerable interest in programminglanguagesthat encode security policies in type declarations. Type-checking is used to determine whether a program enforces these policies. this approach enjoys many of the benefits of static type-checking, but is particularly of interest because it can enforce information flow properties such as noninterference, for which purely dynamic mechanisms are ineffective. Enforcing information flow properties for distributed systems adds a new challenges: mutual distrust among the principals, and untrusted hosts. Our new approach, secure program partitioning, automatically rewrites a program into communicating subprograms that run securely on the set of available hosts yet collectively implement the original program. this fine-grained rewriting is based on the security types in the original program and the trust relationships among principals and hosts in the system. Computation in the original program is written in a single-host style, yet the resulting distributed system can satisfy the strong confidentiality and integrity properties specified by the program.
there is a growing demand for software tools that can assist in designing, analyzing and validating embedded real-time system applications. ESTEREL a synchronous language, is widely used in the development of embedded...
详细信息
ISBN:
(纸本)0769514146
there is a growing demand for software tools that can assist in designing, analyzing and validating embedded real-time system applications. ESTEREL a synchronous language, is widely used in the development of embedded systems and hardware/software codesign. In this paper, we describe a method that uses timed annotations for ESTEREL programs that makes it possible to predict the timing constraints required to be satisfied by the embedded system. Using the specified annotations and the programming environment of ESTEREL we describe a method and a tool for validating the concrete realization relative to time-annotated ESTEREL specifications. Also, the method derives time constraints to be satisfied by the concrete architectures for realizing the logical specification. We shall illustrate the technique with examples as well as the structure of the tool implemented.
Statecharts is a visual language for specifying reactive system behavior. the formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software desi...
详细信息
Statecharts is a visual language for specifying reactive system behavior. the formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, withtheir intuitive operational interpretation. the classical semantics of State-charts, however, suffers from a serious defect: it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability. this paper suggests a new compositional approach to formalizing Statecharts semantics as flattened labeled transition systems in which transitions represent system steps. the approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first presented for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.
the proceedings contain 19 papers. the special focus in this conference is on programminglanguages and systems. the topics include: A decidable logic for describing linked data structures;interprocedural control flow...
ISBN:
(纸本)3540656995
the proceedings contain 19 papers. the special focus in this conference is on programminglanguages and systems. the topics include: A decidable logic for describing linked data structures;interprocedural control flow analysis;a per model of secure information flow in sequential programs;quotienting share for dependency analysis;types and subtypes for client-server interactions;types for safe locking;constructor subtyping;safe and principled language interoperation;deterministic expressions in C;a programming logic for sequential java;set-based failure analysis for logic programs and concurrent constraint programs;simpler, and more expressive;type-based decompilation;an operational investigation of the CPS hierarchy;higher-order code splicing;expressing structural properties as language constructs;polytypic compact printing and parsing and dynamic programming via static incrementalization.
the proceedings contain 36 papers. the special focus in this conference is on Typing and Structuring systems. the topics include: Calculate polytypically;limits of ML-definability;functorial ML;parametric polymorphism...
ISBN:
(纸本)3540617566
the proceedings contain 36 papers. the special focus in this conference is on Typing and Structuring systems. the topics include: Calculate polytypically;limits of ML-definability;functorial ML;parametric polymorphism for typed prolog and a-prolog;a specification formalism for inheritance and object hierarchies;towards independent and-parallelism in CLP;annotated structure shape graphs for abstract analysis of prolog;a reactive implementation of pos using ROBDDs;dynamic attribute grammars;controlling conjunctive partial deduction;unfold/fold transformations of concurrent processes;semantics-based compiling;implementing memoization for partial evaluation;higher order deforestation;scheduling expression DAGs for minimal register need;improving tabled logic programs through alternative scheduling strategies;a new implementation approach for prolog;systematic extraction and implementation of divide-and-conquer parallelism;functional skeletons generate process topologies in eden;a language for executable specifications;from term rewriting to generalised interaction nets;type isomorphisms for module signatures;decidability of logic program semantics and applications to testing;unifying pictures and widgets in a constraint-based framework for concurrent functional GUI;modeling sharing and recursion for weak reduction strategies using explicit substitution;context-sensitive computations in confluent programs;models for using stochastic constraint solvers in constraint logic programming;integrating efficient records into concurrent constraint programming;the LOL deductive database programming language;an efficient and precise sharing domain for logic programs;cheap tupling in calculational form;needed narrowing in prolog;automatic optimization of dynamic scheduling in logic programs and a visual constraint programming tool.
We present a new programming language ProFun which is aimed for the specification and prototype implementation of reactive systems. ProFun combines the paradigms of concurrent and functional programming. A formal oper...
详细信息
this paper proposes a number of models for integrating stochastic constraint solvers into constraint logic programmingsystems in order to solve constraint satisfaction problems efficiently. Stochastic solvers can sol...
详细信息
We present a collection of skeletons that are appropriate to instantiate process systems in the functional-concurrent language Eden [BLOM96]. Eden is a functional language providing facilities for the explicit definit...
详细信息
A new approach in which stateful computations can be performed within the framework of a functional programming language is presented. In most functional programminglanguages, programmers are unable to easily manipul...
详细信息
A new approach in which stateful computations can be performed within the framework of a functional programming language is presented. In most functional programminglanguages, programmers are unable to easily manipulate state-based computations which are not supported by functional languages. To solve this problem, the authors propose to extend the Sisal language with special user declared variables. this approach can greatly help users in writing programs, simplifying parallel compilation, and improving performance. Under this scheme, programmers are able to manipulate stateful computations. In the methodology, programmers are allowed to declare special variables, and the parallel threads can be identified according to the usage of special variables. When compared to "pure" functional languages, the extended Sisal has more expressive power due to the availability of stateful computations.
Symmetry is a parallel programming language intended for specifying scalable computation and communication in (K-1)-dimensions of discrete space and 1-dimension of discrete time. A program specifies causal and geometr...
详细信息
ISBN:
(纸本)0818656026
Symmetry is a parallel programming language intended for specifying scalable computation and communication in (K-1)-dimensions of discrete space and 1-dimension of discrete time. A program specifies causal and geometric relationships between space time regions and indicates when and where each subcomputation takes place. Symmetry unifies the notions of memory and communication in an expanded concept of 'variable'. A Symmetry variable propagates its value in any timelike direction in spacetime, not just in a direction parallel to the time axis as is the case for memory variables in traditional languages. A performance model for Symmetry properly accounts for the all costs of computation including communication delay.
暂无评论