KR101731629B1 - Method and device for automatic generating go code from circus - Google Patents

Abstract

A method for automatically generating a Go code from a Circus specification in an automatic Go code generation device including an input module, an execution code conversion module, and a monitoring code conversion module is disclosed. The Go code automatic generation method includes a Circus specification input step for receiving a Circus specification written in a Circus specification specification language and a Go code generation step for automatically converting the Circus specification to a Go code using a conversion function, A first code conversion process for converting a specification part for a state schema, an operation schema, or a system behavior into a first code that is an actual operating part of the Go code in the Circus specification, And a second code conversion process of converting a portion of the invariants into a second code that is a part for monitoring whether the verification property violates during operation of the first code.

Description

[0001] METHOD AND APPARATUS FOR AUTOMATIC GENERATING GO CODE FROM CIRCUS [0002]

An embodiment according to the concept of the present invention relates to a method and apparatus for automatically generating a Go code, which is a programming language, from a formal specification language, Circus. In particular, Circus's state, operation and behavior specification are part of the Go code And Invariants, which is a verification attribute, converts a working code into a code for monitoring.

This patent proposes a technology to automatically convert to the corresponding Go code based on the specification written in the formal specification language Circus. In other words, it takes the Circus specification as input and automatically generates an executable Go code.

Formal techniques include formal specification and formal verification as techniques for developing computer systems or software using techniques of mathematical or logic-based specification and design. The formal specification is to describe the system operating environment, system requirements, and system design using mathematical logic, etc. Formal verification is a mathematical and logical proof method that demonstrates system design and system requirements. will be.

If the process of implementing the formal specification into software code (source code) is not correct, or the code is written differently from the specification, even if it proves that the formal specification works properly through formal verification, etc., A problem that can not be solved occurs.

In particular, when a developer develops manually based on a formal specification, a developer's mistakes (Human Faults) can occur, and therefore code that does not work as specified can be written. That is, the developer may not understand the formal specification properly or a mistake may be inserted in the code, resulting in the generation of incorrect code.

Therefore, a code conversion method capable of automatically generating an accurate code from a formal specification is required.

"A. It is known that a technology for automatic translation into a programming language in Freitas and A. Cavalcanti, "Automatic Translation from Circus to Java ", In FM 2006, pages 15-130, Springer, 2006 Circus, It does not translate into actual operation part and monitoring part in translation.

US 2002-0062475 A1 US 2009-0089234 A1 KR 2011-0020520 A

The technical problem to be solved by the present invention is to provide a method and an apparatus for automatically generating a Go code as a programming language from a formal specification language Circus.

Also, a method and an apparatus for automatically generating a Go code with high reliability are provided by converting the invariants of Circus into monitoring codes and monitoring the operation of the converted code by using the same.

The method for automatically generating the Go code from the Circus specification according to the embodiment of the present invention includes a Circus specification input step for inputting a Circus specification written in the Circus specification specification language and an automatic conversion process for converting the Circus specification to a Go code using a conversion function The Go code generation step converts the specification part of the state schema, operation schema, or system behavior into the first code, which is an actual operating part of the Go code, in the Circus specification And a second code conversion process for converting a portion of the invariants in the Circus specification to a second code for monitoring whether the verification property violates during operation of the first code, .

The automatic Go code generating apparatus according to the embodiment of the present invention receives the formal specification written in the Circus and automatically generates the Go code corresponding thereto, thereby eliminating the possibility that the developer's mistake is inserted and enhancing the reliability and accuracy of the source code .

In addition, the Go code automatic generation apparatus according to the embodiment of the present invention can generate the Circus-based formal specification specified in various aspects as a whole executable code instead of a skeleton-based code or a function-based code.

In addition, the automatic Go code generating apparatus according to the embodiment of the present invention can monitor whether or not the check attribute is violated during the Go code operation by generating the monitoring code using the invariants of the Circus.

DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENTS In order to more fully understand the drawings recited in the detailed description of the present invention, a detailed description of each drawing is provided.
1 is a functional block diagram of an automatic Go code generating apparatus according to an embodiment of the present invention.
FIG. 2 is a diagram showing a conversion concept of Go code conversion from a formal specification specified as Circus.
3 is a flowchart illustrating a method of automatically generating a Go code from a Circus according to an embodiment of the present invention.
4 is a diagram illustrating a conversion rule of a conversion function according to an embodiment of the present invention.
FIG. 5 illustrates an example of a transform function according to an embodiment of the present invention, and FIG. 6 illustrates an example of a transform function according to an exemplary embodiment of the present invention. Referring to FIG.
FIG. 7A is a diagram illustrating an example of a Circus specification that is an input value of the automatic code generation apparatus according to an embodiment of the present invention, and FIG. 7B is a diagram illustrating a Go code automatically outputting the Circus specification of FIG. .

It is to be understood that the specific structural or functional description of embodiments of the present invention disclosed herein is for illustrative purposes only and is not intended to limit the scope of the inventive concept But may be embodied in many different forms and is not limited to the embodiments set forth herein.

The embodiments according to the concept of the present invention can make various changes and can take various forms, so that the embodiments are illustrated in the drawings and described in detail herein. It should be understood, however, that it is not intended to limit the embodiments according to the concepts of the present invention to the particular forms disclosed, but includes all modifications, equivalents, or alternatives falling within the spirit and scope of the invention.

The terms first, second, etc. may be used to describe various elements, but the elements should not be limited by the terms. The terms may be named for the purpose of distinguishing one element from another, for example, without departing from the scope of the right according to the concept of the present invention, the first element may be referred to as a second element, The component may also be referred to as a first component.

The terminology used herein is for the purpose of describing particular embodiments only and is not intended to be limiting of the invention. The singular expressions include plural expressions unless the context clearly dictates otherwise. In this specification, the terms "comprises" or "having" and the like are used to specify that there are features, numbers, steps, operations, elements, parts or combinations thereof described herein, But do not preclude the presence or addition of one or more other features, integers, steps, operations, components, parts, or combinations thereof.

Unless defined otherwise, all terms used herein, including technical or scientific terms, have the same meaning as commonly understood by one of ordinary skill in the art to which this invention belongs. Terms such as those defined in commonly used dictionaries are to be interpreted as having a meaning consistent with the meaning of the context in the relevant art and, unless explicitly defined herein, are to be interpreted as ideal or overly formal Do not.

Hereinafter, embodiments of the present invention will be described in detail with reference to the drawings attached hereto.

First, the formal specification technique and code used in the present invention will be described.

In the present invention, the formal specification language input for code conversion is Circus. Circus is a language developed by York Univ. In 2000. It is a combination of state-based formal specification language Z and process Algebra CSP. The state of the system and each operation are defined as Z, and system-wide or partial actions are defined using CSP. Circus has the feature that various aspects can be specified by expressing the behavior specification as well as the system functional specification.

Further, in the present invention, the program language used for the result of code conversion is Go code (also called Golang). Go code was developed by Google in December 2009 and is based on the C language and concurrency based on the CSP language in the Golang language design. Golang provides garbage collection and type safety. In particular, there is a feature that provides concurrency by providing high routine, channel, and select statements.

Hereinafter, a Go code automatic conversion apparatus for converting a Circus specification into a Go code according to an embodiment of the present invention will be described in detail with reference to FIGS. 1 and 2. FIG.

1 is a functional block diagram of an automatic Go code generating apparatus 100 according to an embodiment of the present invention. Referring to FIG. 1, the automatic Go code generating apparatus 100 includes an input module 110, a conversion module 120, a monitoring module 130, a memory 180, and a control module 190.

The module used in the present specification may mean a functional and structural combination of hardware for carrying out the technical idea of the present invention and software for driving the hardware. For example, the module may mean a logical unit of a predetermined code and a hardware resource for executing the predetermined code, and does not necessarily mean a physically connected code or a kind of hardware.

The input module 110 of the automatic Go code generating apparatus 100 receives the Circus specification specified in the Circular specification language.

The conversion module 120 converts the Circus formal specification language into a Go code. Concretely, all or some of the specifications of the Circus specification and symbols in the specification are input, and the corresponding code is derived or the input value is transmitted to the corresponding function to eject the final Go code.

The conversion module 120 mainly includes an execution code conversion module 121 (hereinafter referred to as a first conversion module) for generating a code of a portion actually operating in the Go code, and a monitoring code conversion module (123, hereinafter referred to as a second conversion module).

FIG. 2 is a diagram showing a conversion concept of Go code conversion from a formal specification specified as Circus. Referring to FIG. 2, the first conversion module 121 converts a specification related to a state schema, an operation schema, and a system behavior in the Circus formal specification language into actual operation of the Go code (Correct program).

The second conversion module 123 converts invariants, which are verification attributes in the Circus formal specification language, into the invariants at the same time when the code generated by the execution code conversion module 121 is operated, that is, when the program is executed And converts it into a monitoring code (Mornitoring Code) that can be monitored (Runtime Mornitoring) to check whether the verification property is violated.

The verification module 130 monitors the verification property violation while the program code generated by the first conversion module 121 operates using the monitoring code generated by the second conversion module 123. [

The memory 180 may include a program memory and a data memory. Programs for controlling the operation of the automatic Go code generating apparatus 100 may be stored in the program memory. Data generated during the execution of the programs may be stored in the data memory.

The control module 190 controls the overall operation of the automatic Go-code generating apparatus 100. That is, the operation of the input module 110, the conversion module 120, the verification module 130, and the memory 180 can be controlled.

Hereinafter, a method of automatically generating the Go code from the Circus specification using the automatic Go code generating apparatus according to an embodiment of the present invention will be described in detail with reference to FIG. 3 to FIG. 7B.

3 is a flowchart for explaining a method of automatically converting the Circus specification into the Go code.

First, the Go code automatic conversion apparatus receives the Circus specification (S100). Next, although not shown in the figure, it may further include a step of regularly verifying the input Circus specification.

Next, the inputted Circus specification is converted into Go code (S200). Go code conversion step includes an execution code conversion step (or a first code conversion step, S210) and a monitoring code conversion step (or a second code conversion step, S230).

In the first code conversion step S210, the state and operation of the Circus and the behavior specification of the CSP are converted into a first code, which is a code part of the Go code that actually operates. In the second code conversion step S230, Converts invariants to second code, the monitoring code. The second code then uses the verification attribute in monitoring step S300 to monitor for violation.

 Specifically, the code conversion strategy according to an embodiment of the present invention is shown in Table 1.

Translation Strategy Circus golang One System Process Each function (call in the main function) 2 channel channel 3 Status of the state schema Global variables 4 Invariant attributes of state schema Each function (created as a high routine in the main function) 5 Operation schema function 6 State declared in the operation schema Local variables in functions 7 Inputs and outputs declared in the operation schema Input, output of function 8 action function

로 표시한다.In the code conversion step S200 according to an embodiment of the present invention, code conversion is performed through functions. 4 is a diagram illustrating a conversion rule of a conversion function according to an embodiment of the present invention. Referring to FIG. 4, the functions receive symbols corresponding to all or part of the specifications and specifications of Circus, and derive corresponding codes or transfer input values to corresponding functions. The functions are repeatedly performed to derive the final Go code. The Translation Function

.

Hereinafter, with reference to FIG. 5 to FIG. 6, a process of converting each part of the specification written in Circus into Go code will be described. 5 is a diagram showing an example of the conversion function operation according to an embodiment of the present invention.

Referring to Figure 5 (a), for example, the full specification may be a program, which may be AC or B, Also, Syntactic conversion can be done with A as a, B as b, and C as c. If you look at the conversion function, the full specification Program is applied to the Program function. At this time, it is applied to AC function when program is AC, and to B function when B is program. In case of AC, it is applied to A function and C function, respectively, and the program code "&" is added between them. A, B, and C are applied to a, b, and c functions as input values a, b, and c. A, b, and c are applied to the corresponding functions to generate "program code a" , &Quot; program code c "

Referring to FIG. 5 (b), when converting the entire specification called AC, the specification AC is applied to the AC function according to the definition of the program function. The AC function again applies A to the A function, C to the C function, and inserts the program code & in the middle. A and C are applied to A and C functions, respectively, and input values a and c are applied to a and c functions, and "program code a" and "program code c" are derived. Finally, the code "Program code a & Program code c" is derived.

6 is a diagram illustrating an example of a transform function according to an embodiment of the present invention. The transformation function shown in FIG. 6 defines a transformation for a process definition as a ProcDecl function. When the "process N = ProcDef" input is given to the ProcDecl function, the corresponding Go code (from 'func main {' to '}') is generated and the ProcDef symbol is reapplied to the procDef function in the main function.

Hereinafter, an example of the Go code, which receives the specification written in the Circus and automatically converts and outputs the output, will be described in detail with reference to FIGS. 7A and 7B.

FIG. 7A is an exemplary diagram of a formal specification created with an input value Circus, and FIG. 7B is a diagram illustrating a Go code, which is a result value converted by predefined conversion functions with the Circus specification of FIG. 7A as an input value .

The state v of the state schema is declared as a global variable v, and the operation AddOp is converted to the function AddOp (). Also, the entire action of the process (u X? Out! V -> AddOp; X) is defined by the function Accumulator1Main () and the contents are converted into code in the function. The function v_Type is a type attribute for the state variable v. It is converted into a monitoring code that checks whether the property is violated by executing the code at the same time when the code is executed with the keyword go before the function call. If an immutable attribute is defined in the state schema, it is also executed concurrently and converted to monitoring code.

Next, the Go code is executed and at the same time, the property code violation is monitored using the monitoring code (S300). Generally, during software development, first verify that the Circus specification violates the attributes that must be satisfied. It is possible to secondarily verify whether or not the attribute violation is caused by monitoring using the monitoring code whether or not the attributes to be satisfied are violated during the operation of the automatically converted code in the coding step.

It is possible to automatically generate a more accurate Go code by using the automatic Go code generating device and the Go code automatic generating method according to an embodiment of the present invention and additionally generate a monitoring code to monitor the property violation It is possible to develop more accurate and reliable software.

A method for formally verifying a real-time system in which the scheduler exists in a hierarchical manner can be implemented in a general-purpose digital computer that can be created as a program that can be executed in a computer and operates the program using a computer-readable recording medium have. The program is stored on the recording medium, and the recording medium may be a storage medium such as a magnetic storage medium (e.g., ROM, floppy disk, hard disk, etc.), an optical reading medium (e.g., CD ROM, . In addition, the recording medium may be distributed and distributed to a network-connected computer system so that a computer-readable instruction set can be stored and executed in a distributed manner.

The block diagrams disclosed herein may be construed to those skilled in the art to conceptually represent circuitry for implementing the principles of the present invention. Likewise, any flow chart, flow diagram, state transitions, pseudo code, etc., may be substantially represented in a computer-readable medium to provide a variety of different ways in which a computer or processor, whether explicitly shown or not, It will be appreciated by those skilled in the art.

While the present invention has been particularly shown and described with reference to exemplary embodiments thereof, it is evident that many alternatives, modifications and variations will be apparent to those skilled in the art. Accordingly, the true scope of the present invention should be determined by the technical idea of the appended claims.

100: Go code automatic generation device
110: input module 120: conversion module
130: Monitoring module 180: Memory

Claims (6)

Circus Input module that receives Circus specification written in formal specification language,
A first transformation module for transforming the specification part of the state schema, operation schema, or system behavior into the Go code in the Circus specification, and
A second transform module for transforming the portion of the invariants in the Circus specification to a Go code,
The first transformation module generates a first code which is an actual operating part of the Go code,
Wherein the second conversion module generates a second code for monitoring whether the verification property violates during operation of the first code,
Go code automatic generation device.
The method according to claim 1,
Further comprising: a verification module that, when executing the first code, executes the second code concurrently to monitor whether the verification property violates,
Go code automatic generation device.
A method for automatically generating a Go code from a Circus specification,
A Circus specification input step in which the input module of the Go code automatic generation device receives the Circus specification written in the Circus specification specification language; And
And a Go code generating step of automatically converting the Circus specification into a Go code using a conversion function,
The Go code generation step includes:
A first code conversion step of converting the specification part of the state schema, operation schema, or system behavior into the first code, which is an actual operating part of the Go code, in the Circus specification; And
And a second code conversion process for converting a portion of invariants in the Circus specification to a second code for monitoring whether the verification property violates during operation of the first code.
How to automatically generate Go code from Circus.
The method of claim 3,
Further comprising a monitoring step of, when the verification module of the automatic Go-code generating device executes the first code, simultaneously executing the second code to monitor whether the verification property violates the verification code.
How to automatically generate Go code from Circus.
5. The method of claim 4,
Further comprising: a verification module of the Go code automatic generation device performing a formal verification of the Circus specification.
How to automatically generate Go code from Circus.
The method of claim 3,
The Go code generation step includes:
The system process of the Circus specification converts each function to be called in the main function of the Go code,
The channel of the Circus specification is converted into the channel of the Go code,
The state of the state schema of the Circus specification is converted into a global variable as a channel of Go code,
The invariant attribute of the state schema of the Circus specification is converted into a goroutine function in the main function of Go code,
The operation schema of the Circus specification is converted into a function of Go code,
The state declared in the operation schema of the Circus specification is converted into a local variable in the Go code function,
The input and output declared in the operation schema of the Circus specification are converted to input and output as a function of Go code,
And the action of the Circus specification is converted into a function of Go code.
How to automatically generate Go code from Circus.

Images