Heterogeneous Models of Computation An Abstract Algebra Approach EE249 Lecture Taken from Roberto Passerone PhD Thesis Objectives Provide the foundation to represent different semantic domains for the Metropolis metamodel Study the problem of heterogeneous interaction Formalize concepts such as abstraction and refinement An Example of Interaction Combine a synchronous model with a dataflow model Synchronous model Total order of event Data flow model Partial order of events Discrete Time model Metric order of events An Example of Heterogeneous Interaction The interaction is derived from a common refinement of the heterogeneous models The resulting interaction depends on the particular refinements employed Our objective is to derive the consequences of the interaction at the higher levels of abstraction Data Flow Model Assume signals take values from a set V Each signal is a sequence from V an element of V Let A be the set of signals One behavior is a function f A V A data flow agent is a set of those behaviors a b c d e f g h i j k l Data flow Synchronous Model Signals are again sequences from V elements of V But are synchronized One element of the sequence is g A V One behavior is a sequence of those functions gi A V A synchronous agent is a set of those sequences g1 g2 g3 g4 Synchronous Discrete Time Model Assume time is represented by the positive integers N Then define a behavior h N A V A discrete time agent is a set of those functions 1 2 3 4 Discrete Time Discrete to Synchronous Abstraction a g b j e Synchronous l n p r a b b c e e Discrete g g j j l m n o p p r s Discrete to Data Flow Abstraction a b g c e j lm Data flow n op rs a b b c e e g g j j l m Discrete n o p p r s Interaction Propagation Synchronous U1 Data flow T2 T1 U2 V1 V W1 V2 W2 Discrete 1 2 3 4 Refinement Composition Projection Abstraction Objectives Provide a semantic foundations for integrating different models of computation Independent of the design language Not just specific to the Metropolis meta model Maximize flexibility for using different levels of abstraction For different parts of the design At different stages of the design process For different kinds of analysis Support many forms of abstraction Model of computation model of time synchronization etc Scoping Structure hierarchy Overview Pre Post Process Networks Data Flow P1 pX pZ M M Non metric Time Discrete Time P2 pX pZ M S P1 pZ write P2 pX read Meta Model Continuous Time Agent Algebras Conservative Approximations Domain of agents with operations projection renaming and composition Scope Concentrate on Natural semantic domains sets of agents Relations and functions over semantic domains Relationships between semantic domains and their relations and functions Defer worrying about specific abstract syntaxes and semantic functions Convenient for manual formal reasoning De emphasizing executable and finitely representable models for now Agents and Behaviors For each model of computation we always distinguish between the domain of individual behaviors the domain of agents For different models of computation individual behaviors can be very different mathematical objects We always call these objects traces The nature of the elements of the carrier is irrelevant An agent is primarily a set P of traces We call them trace structures Also includes the signature T P Trace and Trace Structure Algebras Model of individual behaviors A trace structure contains a set of traces Set of traces C Model of agents semantic domain Set of trace structures A Trace algebra Trace structure algebra Projection Renaming Concatenation Composition Scoping Instantiation Essential Elements Must be able to name elements of the model Variables actions signals states We do not distinguish among them and refer to them collectively as a set of signals W Each agent has an alphabet and a signature Alphabet A W Signature A I O etc The operations on traces and trace structures must satisfy certain axioms The axioms formalize the intuitive meaning of the operations They also provide hypothesis used in proving theorems Trade off between generality and structure Metric Time Traces VR VN MI MO x d f f v 0 d R f n 0 d N f a 0 d 0 1 Model time as a metric space Can talk about the difference in time between points in the behavior in quantitative terms Able to specify timing constraints in quantitative terms Able to represent continuous as well as discrete behavior Projection and renaming easily defined on the functions Metric Time Model Traces A trace x models one execution of a hybrid system Signature VR real valued var s VN integer valued var s MI input actions MO output actions The alphabet A of x is the union of the components of d is a non negative real number Length in time of x Can be infinity f gives values as a function of time f VR 0 d R f VN 0 d N f MI 0 d 0 1 f MO 0 d 0 1 Metric Time Model Operations on Traces Let x proj B x represents scoping B is a subset of A concatenation and f are restricted to variables and actions in B d d Let x rename r x Let x x x represents instantiation r is a one to one function with domain A variables and actions in and f are renamed by r d d represents sequential composition d is finite and end of x matches beginning of x d d d f v t is equal to f v t for t d f v t d for t d Metric Time Model Trace Structures A trace structure T P models a process or an agent of a hybrid system P is a set of traces with signature Traits T refines T if P P Natural model for physical components such as those described with differential equations possibly with discrete control variables Too detailed for many other aspects of embedded systems Not a finite representation Finite representations synthesis and verifications algorithms are clearly important but not a focus of this class Trace structures constructed the same way for any trace algebra Metric Time Model Operations on Trace Structures Let T proj B T B is a subset of A is restricted to variables and actions in B combines and P maximal set s t P proj A P P proj A P P proj B P Let T rename r T Let T T T par comp r is a one to one function with domain A variables and actions in are renamed by r P rename r P Let x x x seq comp P P P roughly Non metric Time Traces VR VN MI MO x L m t VR R VN N M 0 1 Model time as a non metric space Can only talk about precedence in time including dense time Based on Totally Ordered Multi Sets Totally ordered vertex set V Labeling function from the vertex set V to …
View Full Document
Unlocking...