Last Update ($Date: 2014/02/24 04:16:40 $)
Yoshiura Laboratory researches computer science, especially temporal logic and relevant logic for software engineering. Yoshiura Laboratory also focuses on a pratical investigation of computer network, computer security and IT systems. The following explains the detail of researches of Yoshiura Laboratory.
Almost all software of social infrastructure is a reactive system, whch interacts with users of the software and provides services to the users. Constrol systems of air planes, operating systems and ATM of banks are examples of reactive systems.
In construction and verification of reactive systems, specifications are important. Especially, formal descriptions of specifications are useful because software can be constructed and verified by formal methods from the formal descriptions of specifications. Temporal logic is one of the formal description languages and there are several tools of verification of software. SMV and SPIN are tools of verfication and they use temporal logic.
SMV and SPIN are called model checker; these tools check whether software satisfies the properties that the software satisfy. The users of the tools describe the properties by temporal logic. SMV and SPIN are useful tools, but these tools can deal with simple properties. In the future, these tools will be able to deal with more complicated properties. Complicated properties come closer to specification of software than simple properties. At that time in the future, checking whether software satisfies the properties requires checking whether the properties are correct.
In addition to model checking, realizability of specification and construction of software from specification have been researched. There are several tools that checking realizability of specification and constructs software from specification. Lily is one of tools. This tool uses temporal logic to describe specifications and checks whether the specifications that are described in temporal logic are realizable. A specification are realizable if and only if there is a software that satisfies the software. Unlike numerical computation programs, specifications of reactive systems are difficult to describe because reactive systems interact with users to provide services to users and cannot understand or predict all behaviors of users. This is to say, reactive systems are open systems while numerical computation programs are closed programs. Therefore, if specifications of reactive systems are descibed without consideration, it is impossible to construct software from the specifications. For example, an elevator system is one of reactive systems and the following specifcation of an elevator cannot be realized.
The elevator system that satisfies this specifcation does not move en elevator box while open button of the door is pushed. Under this condition, if someone pushes a down button at the fifth floor, an elevator box does not go to the fifth floor. Therefore, there is no elevator system that satisfies the specifcation. This specifcation is a simple description and stands on the tacit assumption that one keeps pushing the open button of the the elevator box. Therefore, this specification does not explicitly include this assumption. Checking realizability of reactive systems is detecting tacit assumptions and lacks of specifications. This detection is necessary to construct reactive systems from specifications.
There are several methods that check realizability of specifications and construct software from specifications. These method, however, use automata theory and require much time and much memory. Therefore, it can be used only for small specifications and not for many areas of reactive systems. Yoshiura Laboratory constructs and improves the method of deciding realizability of specifications that are described in temporal logic. The detail is in the following.
Control of information includes censorship of the Internet. Great firewall of China is one of the famous censorship systems. There is a possibility that search engine censors search engine results. In fact, search engine results are censored in the case that the search engine results includes some contents that are related with copyright violatiton, child porno, slander or whistle blowing. However, some of whistle blowing may be necessary and such censorship gives discussion.
Yoshiura Laboratory researches the method of analyzing tendencies and properties of search engine results. Yoshiura Laboratory developed the system that detect webpages that are deleted on search engine results in Japan. This system gives some properties of search engine results, but the properties are not enough to analyze tendencies of search engine results. Yoshiura Laboratory researches the methods of analyzing search engine results in additon to censorship.
Yoshiura Laboratory cooperates with Fujii Laboratory in Gunma University to develop surveillance cameras that do not violate privacy. In our researches, some surveillance cameras have been commercialized and some patents have been obtained. You can see the detail in the homepage The e-JIKEI Network Promotion Institute where Yoshiura is a vice president.
Japan seems to have ten million street lamps. Almost all of the street lamps are controlled only by illumination sensors and even in a neat housing estate, the street lamps turn on at all hours of night. In the midnight, even if no car or pedestrian goes through an area, street lamps turn on.
Yoshiura Laboratory cooperates with Fujii Laboratory in Gunma University to develop energy saving street lamps.