Abstract This study addresses the problem of scheduling machining operations in a highly automated manufacturing environment while considering the work styles of workers. In actual manufacturing, many aspects of the operation must be considered, such as constraints related to the works to be machined in the machining schedule and the states of the workers. To derive good solutions for such a large-scale problem with many constraints within a realistic amount of computation time, we develop an optimization technique based on a mixed-integer programming (MIP)-based large neighborhood local search method for the machining scheduling problem. Then, computer experiments on a problem based on actual machining requirements are performed to verify the validity of the proposed method.

The autonomous vehicle control system is a typical kind of hybrid system that combines both continuous and discrete behavior.Formal specification and verification techniques help us to verify desired properties of given systems.In this study, we propose a way to describe a formal specification of an autonomous vehicle control system in CafeOBJ algebraic specification language.The control system is a hybrid system with continuous variables of time, velocity, and position controlled by discrete pedal actions including acceleration, braking, and no-operation.We also verify the safety property of the autonomous vehicle control system by a theorem proving technique called the proof score method *

The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control.The LJPL protocol has been specified and verified formally using the Maude model checker.Because of the limitation of computation, the existing model checking approach restricts the number of vehicles participating the protocol.In this paper, we model the LJPL protocol as an observational transition system, describe its specification in CafeOBJ, the algebraic specification language, and verify its safety property using the proof score method, where mutual exclusiveness can be proved for an arbitrary number of vehicles * .

Hybrid systems combine both continuous and discrete behaviors.Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports.In this paper, we propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system in CafeOBJ algebraic specification language and verify it by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.

Hybrid systems combine both continuous and discrete behaviors, which occur frequently in safety-critical applications in various domains including Internet-of-Things (IoT) and Cyber-Physical Systems (CPS) applications such as health care, transportation, and robotics. For safe and reliable information society with IoT and CPS technologies, it is important to establish a way to specify and verify hybrid systems formally. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. We propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system (OTS) in CafeOBJ algebraic specification language. OTSs are models where systems behaviors are described through observations. CafeOBJ supports specification execution based on a rewrite theory. We verify that OTS/CafeOBJ specifications of hybrid systems satisfy desired property by the proof score method based on equational reasoning implemented in CafeOBJ interpreter. In this paper, we specify a signal control system with an arbitrary number of vehicles by our proposed method, and verify the system satisfies a safety property by the proof score method.

We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. The proposed method has some notable features. Among them are as follow: (1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and (2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite. Crème is a tool based on the proposed method. We also report on two case studies in which (1) Crème proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and (2) Crème finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property.

Chocolat/SMV is a translator that takes a CafeOBJ specification of a transition system called an OTS and generates an SMV specification of a finite version of the OTS. The primary purpose of the translation is to find errors lurked in CafeOBJ specifications of OTSs with SMV.