Search results for: Michiyoshi Hayase

Authors: Akie Nimiya, Tomoyuki Yokogawa, Hisashi Miyazaki, Sousuke Amasaki, Yoichiro Sato, Michiyoshi Hayase

Abstract:

In this paper, we proposed a method for detecting consistency violation between UML state machine diagrams and communication diagrams using Alloy. Using input language of Alloy, the proposed method expresses system behaviors described by state machine diagrams, message sequences described by communication diagrams, and a consistency property. As a result of application for an example system, we confirmed that consistency violation could be detected using Alloy correctly.

Keywords: Model checking, UML, state machine diagrams, communication diagram, alloy.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1582

Authors: Yuka Kawakami, Tomoyuki Yokogawa, Hisashi Miyazaki, Sousuke Amasaki, Yoichiro Sato, Michiyoshi Hayase

Abstract:

In this paper, we proposed a method for detecting consistency violation between state machine diagrams and a sequence diagram defined in UML 2.0 using SMV. We extended a method expressing these diagrams defined in UML 1.0 with boolean formulas so that it can express a sequence diagram with combined fragments introduced in UML 2.0. This extension made it possible to represent three types of combined fragment: alternative, option and parallel. As a result of experiment, we confirmed that the proposed method could detect consistency violation correctly with SMV.

Keywords: UML, model checking, SMV, sequence diagram.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1469

Authors: Masafumi Kondo, Yoichiro Sato, Kazuyuki Tashiro, Tomoyuki Yokogawa, Michiyoshi Hayase

Abstract:

Recently, most digital systems are designed as GALS (Globally Asynchronous Locally Synchronous) systems. Several architectures have been proposed as bus architectures for a GALS system : shared bus, segmented bus, ring bus, and so on. In this study, we propose a ring segmented bus architecture which is a combination of segmented bus and ring bus architecture with the aim of throughput enhancement. In a segmented bus architecture, segments are connected in series. By connecting the segments at the end of the bus and constructing the ring bus, it becomes possible to allocate a channel of the bus bidirectionally. The bus channel is allocated to the shortest path between segments. We consider a metastable operation caused by asynchronous communication between segments and a burst transfer between segments. According to the result of simulation, it is shown that the GALS system designed by the proposed method has the desired operations.

Keywords: GALS systems bus architecture, segmented bus, ring bus.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1137