The Experts below are selected from a list of 321 Experts worldwide ranked by ideXlab platform
Kyunghee Choi - One of the best experts on this subject based on the ideXlab platform.
-
modeling software requirement with Timing Diagram and simulink stateflow
Information & Software Technology, 2011Co-Authors: Hongsuk Lee, Kihyun Chung, Hyunsang Park, Kyunghee ChoiAbstract:ContextA methodology is needed to model software specification with both Timing Diagram and Simulink/Stateflow (SL/SF) and to convert Timing Diagram model into SL/SF model. ObjectivesThis paper aims to propose a Timing Diagram drawing method and the algorithm to convert a Timing Diagram model into the equivalently behaving SL/SF model. MethodWe add a few extra features to those of the typical Timing Diagrams. The extra features were chosen by the field engineers' requests and the survey of many different commercial models. This paper proposes the formal method to describe the Timing Diagram. Based on the formal description, the converting algorithm translates a Timing Diagram into the SL/SF model. ResultsBy providing a path from Timing Diagram to SL/SF, system specifications can be described with both SL/SF and Timing Diagram. This paper addresses the details of outcomes that the proposed method was successfully applied to modeling "Theft watch system" and "Automotive power window controller. The proposed method has been successfully applied to other commercial systems, and to the models provided by Mathworks. ConclusionThis paper proposed a methodology to describe system specification with both Timing Diagram and SL/SF. The strategy might help designers more efficiently describe specifications. In addition, the mixed specification can be simulated in SL/SF, and the specification can utilize other third party SL/SF tools such as test case generation or model check utilities.
-
Test Input Sequence Generation Strategy for Timing Diagram using Linear Programming
The Kips Transactions:partd, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee ChoiAbstract:Timing Diagram is popularly utilized for the reason of its advantages; it is convenient for Timing Diagram to describe behavior of system and it is simple for described behaviors to recognize it. Various techniques are needed to test systems described in Timing Diagram. One of them is a technique to derive the system into a certain condition under which a test case is effective. This paper proposes a technique to automatically generate the test input sequence to reach the condition for systems described in Timing Diagram. It requires a proper input set which satisfy transition condition restricted by input waveform and Timing constraints to generate a test input sequence automatically. To solve the problem, this paper chooses an approach utilizing the linear programming, and solving procedure is as follows: 1) Get a Timing Diagram model as an input, and transforms the Timing Diagram model into a linear programming problem. 2) Solve the linear programming problem using a linear programming tool. 3) Generate test input sequences of a Timing Diagram model from the solution of linear programming problem. This paper addresses the formal method to drive the linear programming model from a given Timing Diagram, shows the feasibility of our approach by prove it, and demonstrates the usability of our paper by showing that our implemented tool solves an example of a Timing Diagram model.
-
test case generation strategy for Timing Diagram
The Kips Transactions:partd, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee ChoiAbstract:Timing Diagram is a useful tool for describing the specification of system, but there is no study for test case strategy of a Timing Diagram. To solve this problem, we followed the steps to generate test cases from Timing Diagram in this paper. 1) We defined a Timing Diagram formally. 2) We describe the method of transforming from a Timing Diagram model into a Stateflow model which has an equivalent relationship between a Timing Diagram model and a transformed Stateflow model. 3) We generated test cases from a transformed Stateflow model using SDV which is plugged in Simulink. To show that our approach is useful, we made an experiment with a surveillance model and arbitrary Timing Diagram models. In the experiment we transformed Timing Diagram models into Stateflow models, generated test cases from transformed Stateflow models using SDV, and analyzed the generation results. The conclusion that can be obtained from this study is that Timing Diagram is not only a specification tool but also a useful tool when users are trying to generate test cases based on model.
-
stateflow td a unified modeling formalism of stateflow and Timing Diagram
The Journal of Korean Institute of Communications and Information Sciences, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee Choi, Regular MembersAbstract:Stateflow is a useful system modeling tool, which is frequently used in industry. But Stateflow has defects when users are trying to describe consecutive behaviors or a system's temporal behaviors. Timing Diagram, on the other hand, is a widely used tool of explaining behaviors of a hardware system in electronics. This tool has a merit when specifying consecutive behaviors and temporal behaviors of a system. Thus, this paper suggests , the unified modeling methodology in Stateflow domain integrating Stateflow with Timing Diagram in order to improve the shortcomings of Stateflow. This paper not only explains a technique of integrating both a Stateflow model and Timing Diagram models, and describes advantages of what formalism has, but also shows its convenience using two example systems.
W. D. Tiedemann - One of the best experts on this subject based on the ideXlab platform.
-
Transformation of Timing Diagram specifications into VHDL code
Proceedings of ASP-DAC'95 CHDL'95 VLSI'95 with EDA Technofair, 1995Co-Authors: W. Grass, C. Grobe, S. Lenk, W. D. Tiedemann, Carlos Delgado Kloos, A. Marin, Tomás RoblesAbstract:Timing Diagrams with data and Timing annotations are introduced as a language for specifying interface circuits. In this paper we describe how to generate VHDL from Timing Diagrams in order to get a hardware implementation or simply to get VHDL code for stimuli to be used in a test bench. By giving Timing Diagrams a formal semantics in terms of T-LOTOS, we can apply optimizing correctness-preserving transformation steps. In order to produce good VHDL code on the way to a hardware implementation it is of great importance to introduce structures into the final description that are not automatically derivable from a given specification. The designer is rather asked to assist in introducing a structure by applying a bottom-up interactive synthesis procedure.
-
Introducing structure into behavioural descriptions obtained from Timing Diagram specifications
Microprocessing and Microprogramming, 1993Co-Authors: W. D. Tiedemann, S. Lenk, C. Grobe, W. GrassAbstract:Abstract Communication-dominated hardware is quite naturally specified in terms of Timing Diagrams. By providing Timing Diagrams with a formal semantics in terms of a timed extension of the formal description technique LOTOS, we obtain formalized pure behavioural specifications. Hereupon we apply correctness-preserving transformations, which are initiated by the user's directives and which iteratively lead to structural specifications. These can be further compiled, eg. into VHDL code.
-
an approach to multi paradigm controller synthesis from Timing Diagram specifications
European Design Automation Conference, 1992Co-Authors: W. D. TiedemannAbstract:The author reports on two high-level synthesis methods to derive controller implementations following different design paradigms from a common natural specification by Timing Diagrams. The first method automatically generates a Mealy automaton to be an input for a variety of excellent finite state machine (FSM) design algorithms. The second method supports an interactive bottom-up synthesis of asynchronous designs. Both methods are founded on the same mathematical basis, notably a process calculus. Due to their formal manifestation, every transformation (synthesis step) is verifiable. This leads to guaranteed correct implementations. >
-
EURO-DAC - An approach to multi-paradigm controller synthesis from Timing Diagram specifications
Proceedings EURO-DAC '92: European Design Automation Conference, 1992Co-Authors: W. D. TiedemannAbstract:The author reports on two high-level synthesis methods to derive controller implementations following different design paradigms from a common natural specification by Timing Diagrams. The first method automatically generates a Mealy automaton to be an input for a variety of excellent finite state machine (FSM) design algorithms. The second method supports an interactive bottom-up synthesis of asynchronous designs. Both methods are founded on the same mathematical basis, notably a process calculus. Due to their formal manifestation, every transformation (synthesis step) is verifiable. This leads to guaranteed correct implementations. >
-
EUROCAST - Bus Protocol Conversion: from Timing Diagrams to State Machines
Computer Aided Systems Theory — EUROCAST '91, 1991Co-Authors: W. D. TiedemannAbstract:A designer of hardware systems always has to deal with the somewhat standard task of interfacing system components to a system architecture using different communication protocols. Still there exists little computer aid to support the design of integrated interface circuits today. We present a high level synthesis method to derive interface controller units from the Timing Diagram specifications of the participating communication protocols. Transformation from Timing Diagrams to terms of a process calculus provides a basis to master the conversion problem. If A and B are process behavior terms that represent Timing Diagrams, a third specification X can be derived automatically, where X describes a converter process for A and B. X exists, if there is a solution for the equation A·X=X·B, where “·” is the concurrency operator of the process calculus. The operational semantics of process calculi permits a state-oriented view of the derived converter specification X. From here it is a well-known procedure to synthesize a hardware realization.
Kihyun Chung - One of the best experts on this subject based on the ideXlab platform.
-
modeling software requirement with Timing Diagram and simulink stateflow
Information & Software Technology, 2011Co-Authors: Hongsuk Lee, Kihyun Chung, Hyunsang Park, Kyunghee ChoiAbstract:ContextA methodology is needed to model software specification with both Timing Diagram and Simulink/Stateflow (SL/SF) and to convert Timing Diagram model into SL/SF model. ObjectivesThis paper aims to propose a Timing Diagram drawing method and the algorithm to convert a Timing Diagram model into the equivalently behaving SL/SF model. MethodWe add a few extra features to those of the typical Timing Diagrams. The extra features were chosen by the field engineers' requests and the survey of many different commercial models. This paper proposes the formal method to describe the Timing Diagram. Based on the formal description, the converting algorithm translates a Timing Diagram into the SL/SF model. ResultsBy providing a path from Timing Diagram to SL/SF, system specifications can be described with both SL/SF and Timing Diagram. This paper addresses the details of outcomes that the proposed method was successfully applied to modeling "Theft watch system" and "Automotive power window controller. The proposed method has been successfully applied to other commercial systems, and to the models provided by Mathworks. ConclusionThis paper proposed a methodology to describe system specification with both Timing Diagram and SL/SF. The strategy might help designers more efficiently describe specifications. In addition, the mixed specification can be simulated in SL/SF, and the specification can utilize other third party SL/SF tools such as test case generation or model check utilities.
-
Test Input Sequence Generation Strategy for Timing Diagram using Linear Programming
The Kips Transactions:partd, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee ChoiAbstract:Timing Diagram is popularly utilized for the reason of its advantages; it is convenient for Timing Diagram to describe behavior of system and it is simple for described behaviors to recognize it. Various techniques are needed to test systems described in Timing Diagram. One of them is a technique to derive the system into a certain condition under which a test case is effective. This paper proposes a technique to automatically generate the test input sequence to reach the condition for systems described in Timing Diagram. It requires a proper input set which satisfy transition condition restricted by input waveform and Timing constraints to generate a test input sequence automatically. To solve the problem, this paper chooses an approach utilizing the linear programming, and solving procedure is as follows: 1) Get a Timing Diagram model as an input, and transforms the Timing Diagram model into a linear programming problem. 2) Solve the linear programming problem using a linear programming tool. 3) Generate test input sequences of a Timing Diagram model from the solution of linear programming problem. This paper addresses the formal method to drive the linear programming model from a given Timing Diagram, shows the feasibility of our approach by prove it, and demonstrates the usability of our paper by showing that our implemented tool solves an example of a Timing Diagram model.
-
test case generation strategy for Timing Diagram
The Kips Transactions:partd, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee ChoiAbstract:Timing Diagram is a useful tool for describing the specification of system, but there is no study for test case strategy of a Timing Diagram. To solve this problem, we followed the steps to generate test cases from Timing Diagram in this paper. 1) We defined a Timing Diagram formally. 2) We describe the method of transforming from a Timing Diagram model into a Stateflow model which has an equivalent relationship between a Timing Diagram model and a transformed Stateflow model. 3) We generated test cases from a transformed Stateflow model using SDV which is plugged in Simulink. To show that our approach is useful, we made an experiment with a surveillance model and arbitrary Timing Diagram models. In the experiment we transformed Timing Diagram models into Stateflow models, generated test cases from transformed Stateflow models using SDV, and analyzed the generation results. The conclusion that can be obtained from this study is that Timing Diagram is not only a specification tool but also a useful tool when users are trying to generate test cases based on model.
-
stateflow td a unified modeling formalism of stateflow and Timing Diagram
The Journal of Korean Institute of Communications and Information Sciences, 2010Co-Authors: Hongseok Lee, Kihyun Chung, Kyunghee Choi, Regular MembersAbstract:Stateflow is a useful system modeling tool, which is frequently used in industry. But Stateflow has defects when users are trying to describe consecutive behaviors or a system's temporal behaviors. Timing Diagram, on the other hand, is a widely used tool of explaining behaviors of a hardware system in electronics. This tool has a merit when specifying consecutive behaviors and temporal behaviors of a system. Thus, this paper suggests , the unified modeling methodology in Stateflow domain integrating Stateflow with Timing Diagram in order to improve the shortcomings of Stateflow. This paper not only explains a technique of integrating both a Stateflow model and Timing Diagram models, and describes advantages of what formalism has, but also shows its convenience using two example systems.
E. Cerny - One of the best experts on this subject based on the ideXlab platform.
-
synthesis of checker efsms from Timing Diagram specifications
International Symposium on Circuits and Systems, 1999Co-Authors: E K Ogoubi, E. CernyAbstract:Efficient design verification is a major preoccupation in hardware systems design. We report on a method that assists the verification of the implementations of synchronous bus protocols (e.g., PCI). To this end we convert a Timing Diagram specification of the protocol in the form of hierarchical annotated action Diagrams (HAAD) into synchronous state machines-checkers that can be used to observe the activity on the bus during simulation, emulation or formal verification and signal an error signal if a protocol violation is detected. The checkers are coded in synthesizable RT-level Verilog or VHDL. We illustrate the method on a subset of the PCI bus protocol.
-
ISCAS (1) - Synthesis of checker EFSMs from Timing Diagram specifications
ISCAS'99. Proceedings of the 1999 IEEE International Symposium on Circuits and Systems VLSI (Cat. No.99CH36349), 1999Co-Authors: E K Ogoubi, E. CernyAbstract:Efficient design verification is a major preoccupation in hardware systems design. We report on a method that assists the verification of the implementations of synchronous bus protocols (e.g., PCI). To this end we convert a Timing Diagram specification of the protocol in the form of hierarchical annotated action Diagrams (HAAD) into synchronous state machines-checkers that can be used to observe the activity on the bus during simulation, emulation or formal verification and signal an error signal if a protocol violation is detected. The checkers are coded in synthesizable RT-level Verilog or VHDL. We illustrate the method on a subset of the PCI bus protocol.
-
Verification of real time controllers against Timing Diagram specifications using constraint logic programming
Proceedings 1999 IEEE International Conference on Computer Design: VLSI in Computers and Processors (Cat. No.99CB37040), 1999Co-Authors: E. CernyAbstract:Given a pseudo-synchronous (sampled input) finite-state machine implementation of a real-time controller (e.g., RTL Verilog code), and a Timing Diagrams (TDs) specification, the question we wish to answer is whether the controller satisfies this specification. Our method uses constraint logic programming (CLP). The controller FSM is fed with input sequences derived from the assumption constraints on the inputs as stated in the TD, and its outputs are verified against the required Timing (commit) constraints in the TD. Our technique considers all input sequences in one consistency check for each commit constraint, carried out on a system of constraints constructed from the TD and the unfolded controller FSM. The number of constraints is linear in the lengths of the intervals of the assumption constraints. The method was implemented in CLP (BNR) Prolog which is based on relational interval arithmetic (RIA). We verified a controller for an asynchronous bus.
-
Verificatiom of synchronous realizability of interfaces from Timing Diagram specifications
Proceedings of the Tenth International Conference on Microelectronics (Cat. No.98EX186), 1998Co-Authors: A. El-aboudi, E.-m. Aboulhamid, E. CernyAbstract:We define the realizability of synchronous interface controllers where the specification of the communication is based on Timing Diagrams. A feasible maximum clock period is computed such that all Timing constraints are satisfied. Our algorithm for finding the clock period is based on checking a property of the Timing Diagram that we call local consistency.
-
Synthesis of interface controllers from Timing Diagram specifications
Proceedings of the IEEE 1998 Custom Integrated Circuits Conference (Cat. No.98CH36143), 1998Co-Authors: A. El-aboudi, E.-m. Aboulhamid, E. CernyAbstract:We present a method for verifying the realizability of a Timing Diagram, ensuring the synthesis of the underlying interface is possible. If necessary, a heuristic is introduced to render explicit hidden Timing constraints implied by the specification. A relative schedule of output events is computed, accepting input events from the complete Timing space defined by the assumed constraints on the environment.
Kathi Fisler - One of the best experts on this subject based on the ideXlab platform.
-
Timing Diagrams: Formalization and Algorithmic Verification
Journal of Logic Language and Information, 1999Co-Authors: Kathi FislerAbstract:Timing Diagrams are popular in hardware design. They have been formalized for use in reasoning tasks, such as computer-aided verification. These efforts have largely treated Timing Diagrams as interfaces to established notations for which verification is decidable; this has restricted Timing Diagrams to expressing only regular language properties. This paper presents a Timing Diagram logic capable of expressing certain context-free and context-sensitive properties. It shows that verification is decidable for properties expressible in this logic. More specifically, it shows that containment of ω-regular languages generated by Buchi automata in Timing Diagram languages is decidable. The result relies on a correlation between Timing Diagram and reversal bounded counter machine languages.
-
containing of regular languages in non regular Timing Diagram languages is decidable
Computer Aided Verification, 1997Co-Authors: Kathi FislerAbstract:Parametric Timing constraints are expressed naturally in Timing Diagram logics. Algorithmic verification of parametrically constrained Timing properties is a difficult problem known to be undecidable in most general cases. This paper establishes that a class of parametrically constrained Timing properties can be verified algorithmically against finite-state systems; alternatively stated containment by a regular language is shown decidable for a class of language properties (regular and non-regular) expressible in our Timing Diagram logic.
-
CAV - Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable
Computer Aided Verification, 1997Co-Authors: Kathi FislerAbstract:Parametric Timing constraints are expressed naturally in Timing Diagram logics. Algorithmic verification of parametrically constrained Timing properties is a difficult problem known to be undecidable in most general cases. This paper establishes that a class of parametrically constrained Timing properties can be verified algorithmically against finite-state systems; alternatively stated containment by a regular language is shown decidable for a class of language properties (regular and non-regular) expressible in our Timing Diagram logic.