Withthe increasing acceptance of automation of the lower-level design tasks, designers are increasingly focusing their efforts at the more abstract stages of the system-design process. In this paper, we examine some ...
详细信息
ISBN:
(纸本)0780333020
Withthe increasing acceptance of automation of the lower-level design tasks, designers are increasingly focusing their efforts at the more abstract stages of the system-design process. In this paper, we examine some of the issues related to specification of embedded systems. We first introduce the notion of a conceptual model as being the first step of system specification. We demonstrate the need to have a one-to-one correspondence between the conceptual model and the specification language used to describe the system's functionality We then present some of the salient characteristics of embedded systems Finally, we evaluate the capabilities of several well-known hardware description languages - VHDL, Verilog, Hardware C, SDL (Specification and Description Language), Statecharts, Spec-Charts, and CSP (Communicating Sequential Processes) - with respect to specifying embedded systems.
the proceedings contain 28 papers. the special focus in this conference is on theorem Proving in Higher Order Logics. the topics include: Translating specifications in VDM-SL to PVS;a comparison of HOL and ALF formali...
ISBN:
(纸本)9783540615873
the proceedings contain 28 papers. the special focus in this conference is on theorem Proving in Higher Order Logics. the topics include: Translating specifications in VDM-SL to PVS;a comparison of HOL and ALF formalizations of a categorical coherence theorem;modeling a hardware synthesis methodology in isabelle;inference rules for programming languages with side effects in expressions;deciding cryptographic protocol adequacy with HOL;proving liveness of fair transition systems;program derivation using the refinement calculator;a proof tool for reasoning about functional programs;coq and hardware verification;elements of mathematical analysis in PVS;implementation issues about the embedding of existing high level synthesis algorithms in HOL;five axioms of alpha-conversion;set theory, higher order logic or both;a mizar mode for HOL;towards applying the composition principle to verify a microkernel operating system;a modular coding of unity in coq;importing mathematics from HOL into nuprl;a structure preserving encoding of Z in Isabelle/HOL;improving the result of high-level synthesis using interactive transformational design;using lattice theory in higher order logic;verification of compiler correctness for the WAM;another logic of computable functions;function definition in higher order logic;higher order annotated terms for proof search;a comparison of MDG and HOL for hardware verification and a mechanisation of computability theory in HOL.
In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated reasoning system based on a...
详细信息
ISBN:
(纸本)3540613773
In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated reasoning system based on a Herbrand procedure (enumeration of formula instances) on clauses. the input are arbitrary sentences of first-order logic. the translation into clauses is done incrementally and is controlled by a semantic tableau procedure using unification. this amounts to an incremental polynomial CNF transformation which st the same time encodes part of the tableau structure and, therefore, tableau-specific refinements that reduce the search space. Checking propositional unsatisfiability of the resulting sequence of clauses can either be done with a symbolic inference system such as the Davis-Putnam procedure or it can be done using integer programming. If the latter is used a number of advantages become apparent.
the proceedings contain 63 papers. the special focus in this conference is on Knowledge Representation, Learning and Discovery Systems. the topics include: Learning composite concepts in description logics;comparison ...
ISBN:
(纸本)9783540612865
the proceedings contain 63 papers. the special focus in this conference is on Knowledge Representation, Learning and Discovery Systems. the topics include: Learning composite concepts in description logics;comparison of conceptual graphs for modeling knowledge of multiple experts;semantical considerations for knowledge base updates;partial evaluation in constraint logic programming;the AQI 7-DCI system for data-driven constructive induction and its application to the analysis of world economics;induction of classification rules from imperfect data;induction of expert system rules from databases based on rough set theory and resampling methods;mining patterns at each scale in massive data;on evolving intelligence;intelligent mutation rate control in canonical genetic algorithms;a fine-grained parallel evolutionary program for concept induction;evolutionary exploration of search spaces;evolutionary computation;signed formula logic programming;automating proofs of integrity constraints in situation calculus;towards programming in default logic;on the formal specification of temporal deontic constraints;validity queries and completeness queries;explanation for cooperative information systems;toward intelligent representation of database content;reducing information systems with uncertain attributes;object and dependency oriented programming in FLO;knowledge simplification;a model-based approach to consistency-checking;resource-based vs task-based approaches for scheduling problems;a fuzzy behaviorist approach to sensor-based robot control;knowledge-based fuzzy neural networks;coevolutionary game theoretic multi-agent systems;searching for features defined by hyperplanes;inductive database design and enhancing query processing of information systems.
the proceedings contain 27 papers. the special focus in this conference is on Computer Science Logic. the topics include: Incompleteness of a first-order godel logic and some temporal logics of programs;semantics of n...
ISBN:
(纸本)3540613773
the proceedings contain 27 papers. the special focus in this conference is on Computer Science Logic. the topics include: Incompleteness of a first-order godel logic and some temporal logics of programs;semantics of non-terminating rewrite systems using minimal coverings;congruence types;deduction by combining semantic tableaux and integer programming;a lean evolving algebra compiler;a proof system for finite trees;representing unification in a logical framework;decision procedures using model building techniques;first order logic, fixed point logic and linear order;an evolving algebra abstract machine;languages and logical definability in concurrency monoids;generalized implicit definitions on finite structures;an experiment with instantaneous actions and immediate reactions;a logical aspect of parametric polymorphism;on the modal logic k plus theories;a fully abstract denotational model for observational precongruence;on sharply bounded length induction;effective strategies for enumeration games;bounded fixed-point definability and tabular recognition of languages;equivalences among various logical frameworks of partial algebras;some extensions to propositional mean-value calculus;theorem proving modulo associativity and positive deduction modulo regular theories.
the Prolog program 9;9;term(-)expansion ((define C as A with B), (C-->A:-B,!)). term(-)expansion ((transition E if C then D), ((transition E):-C,!,B,A, (transition(-)))):- rearrange (D,B,A). rearrange ((E,F),...
详细信息
ISBN:
(纸本)3540613773
the Prolog program ''term(-)expansion ((define C as A with B), (C-->A:-B,!)). term(-)expansion ((transition E if C then D), ((transition E):-C,!,B,A, (transition(-)))):- rearrange (D,B,A). rearrange ((E,F), (C,D), (A,B)):- rearrange (E,C,B), rearrange(F,D,A). rearrange (F:=G, ([G]=>*[E], F=..[C/D],D=>*B,A=..[C/B]), asserta(A=>E)). [G/H]=>*[E/F]:- (G=\E;G=..[C/D],D=>*B,A=..[C/B], A=>E), !,H=>*F. square=>*square. A-?B:- [A,B]=.*[D,C], D==C.'' implements an efficient and flexible simulator for evolving algebra specifications.
We have demonstrated a novel method of fabricating Si nanostructures. Based on a combination of atomic force microscope (AFM) field-enhanced oxidation and anisotropic wet chemical etching, Si nanostructures with a min...
详细信息
We have demonstrated a novel method of fabricating Si nanostructures. Based on a combination of atomic force microscope (AFM) field-enhanced oxidation and anisotropic wet chemical etching, Si nanostructures with a minimum width of 50 nm are successfully obtained within the intended area with precise alignment. Overlay patterning followed by AFM field-enhanced oxidation is carried out with high accuracy. It is confirmed that the field-enhanced oxide line with a thickness of at least about 3 nm can act as an mask against anisotropic wet chemical etching. this method enables the realization of sub-10 nm Si nanostructures.
We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is...
详细信息
ISBN:
(纸本)3540613773
We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-terminating systems to this minimal covering. these include the existence of normal forms for arbitrary rewrite systems, and their uniqueness far confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated withthe rules when seen as equations. this extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders, and then instantiate these to term rewriting systems.
Much of the work on verifying software has been done on simple, often artificial, languages or subsets of existing languages to avoid difficult details. In trying to verify a secure application written in C, we have e...
详细信息
暂无评论