Supervisory Control Of Black-box Software Systems Based On Automaton Learning

To save cost in software development of complex systems,legacy systems or third-party components are usually reused,which are often black-boxes without source code or log-ical models.In software engineering practice,requirements are often given in natural or semi-formal languages.It is a difficult task to build an appropriate automaton model for the requirements.When the automaton models of the systems or requirements or both are un-known,this thesis presents some novel supervisor synthesis approaches for the systems by integrating supervisor control theory(SCT)of discrete-event systems(DES)and automaton learning algorithms together.The synthesized supervisors are patched to the systems to en-force them to act as required without modifying the source code of the reused components.The main contributions are listed as follows.When the automaton model of requirements is unavailable but the models of the plant are easy to obtain,an approach is proposed to synthesize supremal nonblocking supervisors for systems by integrating an learning algorithms adapted from the classical L~*algorithm and SCT.This approach consists of two steps.Firstly,a tentatively correct supervisor is inferred by the proposed learning algorithm.If the tentatively correct supervisor is nonblocking,it is indeed the supremal nonblocking supervisor with respect to the system and requirements.Otherwise,the inferred blocking automaton is regarded as a new plant,and the requirement is the nonblocking property.Then,the supremal nonblocking supervisor with respect to the system is computed by SCT.The effective of the approach is illustrated on an automated guided vehicle(AGV)system.When the formal model of the system is unknown but the formal models of the specifica-tions are easy to obtain,SCT and learning-based testing(LBT)technology are integrated together to synthesize supervisors for black-box systems.This approach consists of four steps.Firstly,if the black-box system contains continuous data,they are abstracted to be discrete ones.Secondly,the method employs LBT to verify whether the system meets al-l design requirements.Meanwhile,LBT generates approximate automaton models for the system under test.Subsequently,if the system fails the test,the learned model is applied as the plant model for control synthesis using SCT.Finally,the supervisor is implemented as an executable program to monitor and control the system to follow the requirement.The effectiveness of the proposed method is demonstrated with a brake-by-wire(BBW)software component with floating-point data types.When automaton models of both the system and requirements are unknown,an approach to the control of black-box software systems is proposed by integrating the automaton learning algorithm and SCT together.The approach consists of five steps.Firstly,if the system is continuous,it is abstracted to be discrete.Secondly,the system is tested by some software testing technologies.If all the requirements are satisfied,no supervisor is needed and the process terminates.Otherwise,the procedure proceeds to the third step.The L~*learning algorithm is modified to infer a Moore automaton describing the conjunctive behavior of the system and the requirements.Subsequently,a supremal nonblocking supervisor for the system is derived from the learned Moore automaton.Finally,the supervisor is patched on the system to force the system to satisfy the requirements.The effectiveness of the proposed method is verified by the BBW system and a two-vehicle platooning program.