Search

This paper proposes a concurrent periodic EFSMs model and a technique to synthesize hardware circuits from real-time system specifications in this model. In the proposed model, the data exchange by synchronous execution of the same events in multiple EFSMs (multi-way synchronization) can be specified like LOTOS. The executable time range of each event can be specified as a logical conjunction of linear inequalities of the execution time of its preceding events, constants and integer variables with some values input from environments. Here, we assume that every event sequence starting from the initial state in each EFSM returns to the initial state in the specified time interval. The proposed synthesis technique implements only executable combination of branches in a given specification with a schedule table which guarantees that if each I/O event is executed within the specified time range, at least one of the following event sequences remains executable. Some experiments show that the performance and size of the generated circuits are reasonable for practical use.

Recently various real-time communication protocols have been proposed. In this paper, first, we propose a timed I/O automaton model so that we can simply specify such real-time protocols. The proposed model can handle not only time but also data values. Then, we propose a conformance testing method for the model. In order to trace a test sequence (I/O sequence) on the timed I/O automaton model, we need to execute each I/O action in the test sequence at an adequate execution timing which satisfies all timing constraints in the test sequence. However, since outputs are given from IUTs and uncontrollable, we cannot designate their output timing in advance. Also their output timing affects the executable timing for the succeeding I/O actions in the test sequence. Therefore, in general, the executable timing of each input action in a test sequence can be specified by a function of the execution time of the preceding I/O actions. In this paper, we propose an algorithm to decide efficiently whether a given test sequence is executable. We also give an algorithm to derive such a function from an executable test sequence automatically using a technique for solving linear programming problems, and propose a conformance testing method using those algorithms.

In this paper, we propose a technique for hardware implementation of protocol specifications in LOTOS. For the purpose, we define a new model called synchronous EFSMs consisting of concurrent EFSMs and a finite set of multi-rendezvous indications among their subsets, and propose a conversion algorithm from a subset of LOTOS. The derived synchronous EFSMs can be easily implemented as a synchronous sequential circuit where all the modules corresponding to the EFSMs work synchronously with the same clock. By applying our technique to the Abracadabra protocol, it is confirmed that the derived circuit handles multi-rendezvous efficiently.

In this paper, we propose an implementation method for specifications of distributed systems described in a subclass of LOTOS where operators such as choice and disabling can be used in combination with multi-rendezvous among remote processes. A LOTOS specification with the assignment of each process to a node is implemented as a set of executable codes which run on the corresponding nodes cooperating with each other by exchanging messages. The processes assigned to a node are transformed into a multi-threaded C code by our existing LOTOS compiler. Here, we focus on bus topology networks where broadcasted messages are received at all nodes in the same order, and propose a technique to implement multi-rendezvous among remote processes located on different nodes. We have also extended our LOTOS compiler to generate a set of C codes running on Ethernet. Some experimental results show that typical distributed systems can be described and implemented efficiently.

In this paper, we propose an effective conformance testing method for a subclass of protocols modeled as a set of DFSMs. The number of test cases in the proposed method is only proportional to the sum of those of states and transitions in a given set of DFSMs. In our method, we find a characterization set for each DFSM, which is used to test the DFSM alone in WP-method, and the union of the characterization sets is used as a characterization set for the total system. For a set of DFSMs with common inputs, there may exist two or more tuples of states that have correct responses against a given characterization set. So, in order to identify each state s in a DFSM, we find a characterization set with some specific properties. Then we select a suitable tuple of states containing the state s, and identify the state s by checking their response to the characterization set.

Many communication protocols are modeled as finite state machines (FSM’s). In general, the size of states becomes large in order to treat parameter values such as sequence numbers, and the state explosion may occur. In this paper, we will propose an FSM/C model where the executability of each transition may depend on the number of times that its starting state has been visited, and propose a technique for verifying a liveness property for the model where we avoid the state explosion. For verifying the liveness property, we use an integer linear programming technique.

Verification of timed bisimulation equivalence is generally difficult because of state explo- sion caused by concrete time values. In this paper, we propose a verification method to verify timed bisimulation equivalence of two timed processes using a symbolic technique similar to (Hennessy and Lin 1995). We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System(A-TSLTS). In A-TSLTS, each state has some parameter variables and those values determine its behaviour. Each tran- sition in an A-TSLTS has a guard predicate. The transition is executable if and only if its guard predicate is true under specified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS to make the state-pair be timed bisimulation equivalent. We also show that this result can be applied to the language LOTOS/T(Nakata et al. 1994), a timed extension of LOTOS(ISO 1989).

In this paper, we propose an implementation method of LOTOS specifications using a portable multithread mechanism. Based on the method, we have developed a LOTOS compiler generating efficient and portable object codes. In a generated object code, multiple run-time units in a behaviour expression are executed as threads where run-time units correspond to concurrently executable sub-expressions in the behaviour expression. To keep the temporal ordering of events among run-time units, we create a control area referred by all run-time units in the object code. Each unit refers the area to decide whether each event can be executed or not. If executable, the unit executes the event after modifying the control area. Otherwise, it kills itself when it need not execute the event. Our compiler can also generate efficient codes for a sub-class of the abstract data types (ADTs) in the LOTOS specifications. If the ADT part can be treated as functional programs, the compiler generates as efficient object codes as those written in C language directly. From some experimental results, we show our method is efficient to implement a wide class of LOTOS specifications.

Recently, some studies for developing hardware circuits using LOTOS as a hardware description language have been proposed. In this paper, we introduce a LOTOS-like language called LOTOS/HD. Although LOTOS/HD can treat I/O parameters, LOTOS/HD expressions are functionally closed to Basic LOTOS expressions whose LTS’s are finite. Then, we propose a technique for synthesizing hardware circuits semi-automatically from LOTOS/HD expressions. As the target circuits, synchronous sequential circuits are considered. In the proposed technique, first, the designers describe a specification S of a synchronous sequential circuit in LOTOS/HD where they only describe which values should be calculated and how such values are calculated using some functions implemented as combinational logic circuits. Next, from the data dependency relations and the temporal ordering of the events in S, a candidate C of sequential circuits implementing S is derived where C is also written in LOTOS/HD. The derived circuit C is a correct implementation of S if C satisfies some conditions. If C does not satisfy the conditions, the designers must modify C so that the conditions hold. The variables and functions in C are allocated to the registers and combinational logic circuits, respectively. Using a data path allocation technique, the connections between their components are decided automatically.

In this paper, we propose an automatic test case derivation method for an extended finite state machine model called EFSM/pres where extended UIO sequences called E-UIO sequences are generated. In the EFSM/pres model, each EFSM has a finite control and a finite number of registers where the data types of I/O data and registers’ values are restricted to the integer type. The next registers’ values are represented as linear combinations of the input values and current register values. The transition conditions on input variables and register variables are written using addition, subtraction, comparison and Boolean operators. For such a restricted class, we enumerate every transition sequence and decide whether the sequence is an E-UIO sequence for a given state mechanically. Concrete data values for the E-UIO sequence are also generated mechanically where a decision procedure for Presburger arithmetic is used. The derivation of E-UIO sequences for a part of OSI Session protocol is given as an example.