CN104461882A - Method for model verification of software conforming to DO-178B/C A level - Google Patents
Method for model verification of software conforming to DO-178B/C A level Download PDFInfo
- Publication number
- CN104461882A CN104461882A CN201410728455.5A CN201410728455A CN104461882A CN 104461882 A CN104461882 A CN 104461882A CN 201410728455 A CN201410728455 A CN 201410728455A CN 104461882 A CN104461882 A CN 104461882A
- Authority
- CN
- China
- Prior art keywords
- verification
- model
- proving program
- collection
- definition
- Prior art date
- Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
- Granted
Links
- 238000012795 verification Methods 0.000 title claims abstract description 89
- 238000000034 method Methods 0.000 title claims abstract description 44
- 238000006243 chemical reaction Methods 0.000 claims description 20
- 230000002159 abnormal effect Effects 0.000 claims description 3
- 239000012141 concentrate Substances 0.000 claims description 3
- 238000012546 transfer Methods 0.000 claims description 3
- 238000010200 validation analysis Methods 0.000 claims description 3
- 238000012797 qualification Methods 0.000 abstract description 2
- 230000009466 transformation Effects 0.000 abstract 1
- 230000006870 function Effects 0.000 description 10
- 230000006399 behavior Effects 0.000 description 3
- 101000699762 Homo sapiens RNA 3'-terminal phosphate cyclase Proteins 0.000 description 2
- 102100029143 RNA 3'-terminal phosphate cyclase Human genes 0.000 description 2
- IWUCXVSUMQZMFG-AFCXAGJDSA-N Ribavirin Chemical compound N1=C(C(=O)N)N=CN1[C@H]1[C@H](O)[C@H](O)[C@@H](CO)O1 IWUCXVSUMQZMFG-AFCXAGJDSA-N 0.000 description 2
- 230000015572 biosynthetic process Effects 0.000 description 1
- 238000013461 design Methods 0.000 description 1
- 238000011161 development Methods 0.000 description 1
- 238000000605 extraction Methods 0.000 description 1
- 239000004615 ingredient Substances 0.000 description 1
- 238000012423 maintenance Methods 0.000 description 1
- 238000012827 research and development Methods 0.000 description 1
- 238000004088 simulation Methods 0.000 description 1
- 238000013517 stratification Methods 0.000 description 1
Landscapes
- Stored Programmes (AREA)
Abstract
The invention discloses a method for model verification of software conforming to a DO-178B/C A level, and the method is used for solving the problem of model verification of software development based on a model. The method mainly comprises the following steps: 1) building a verification system framework; 2) converting a model to be verified into a plurality of feature models through a model transformation device; 3) inputting the feature models into data verifying and logic generating layers to generate a data verifying set and a logic verifying set; 4)integrating the data verifying set and the logic verifying set to generate a program verifying set, and selecting a program verifying subset from the program verifying set; 5) according to the program verifying subset, verifying through a software covering intensity level required by DO-178B/C. A powerful support is provided for the airworthiness qualification and certification of vehicle-mounted software by the method.
Description
Technical field
The invention belongs to computer software design technical field, relate to a kind of model automatization verification method, be specifically related to a kind of model verification method meeting DO-178B/C A level software.
Background technology
DO-178B/C " software consideration in mobile system and equipment certification " is US Airways radio
the councilthe aviation Certification standard that (The Radio Technical Commission for Aeronautics, RTCA) proposes, A level is the highest level of Airborne Software development requires.RTCA in 1992 has issued DO-178B " software consideration in mobile system and equipment certification ".DO-178C promulgates in Dec, 2012 and performs.Compared with DO-178B, DO-178C proposes the target call to particular problem or technical method, as instrument qualification, object-oriented method, model developing method etc., formalization method etc. by the form of annex while the stability of the main part of the standard of guarantee.Airborne Software exploitation meets the requirement of DO-178B/C standard, is its necessary condition by the airborne use of certification.The research and development of A level software, according to the requirement of DO-178B/C, are divided into software project, software development and software synthesis three processes.In the software project stage, need plan software life-cycle, software development, verification environment.In software development process, need executive software demand, Software for Design, Software Coding and Integrated Simulation; Executive software checking, software configuration management, software quality assurance and the contact of software certification is needed in combined process.DO-178B/C standard define only the target call of said process, but and which kind of method of not mentioned employing performs these processes.
Summary of the invention
In order to solve the problem in background technology, based on the model development technology that the present invention proposes in DO-178B/C, propose a kind of model verification method meeting DO-178B/C software and can generate software model by Current software modeling tool, according to software level, generate the proving program collection meeting airworthiness requirement, the seaworthiness certification for Airborne Software provides and provides powerful support for.
Concrete technical scheme of the present invention is:
Meet a model verification method for DO-178B/C A level software, it is characterized in that, comprise the following steps:
1) verification system framework is built;
Described verification system framework comprises model conversion layer, verification msg and logic generation layer, proving program generates and chooses layer;
Input model is converted to several characteristic models by model conversion device by described model conversion layer; The transfer process of described model conversion device is the process of data type modeling and feature services modeling;
Several characteristic modules are generated verification msg collection respectively by verification msg maker by described verification msg generation layer, generate verifying logic collection by verifying logic maker;
Described proving program generates and select layer to be generated by proving program and verification msg collection and verifying logic collection are generated as proving program collection by selector switch;
2) user is by mode input to be verified in model conversion layer, and model to be verified is converted to several characteristic models by model conversion device;
3) input to verification msg and logic generation layer with several characteristic models and generate verification msg collection and verifying logic collection by verification msg maker and verifying logic maker;
4) utilize proving program to generate and select the proving program generation in layer and selector switch that verification msg collection and verifying logic collection are generated proving program collection; Concentrate from proving program and select proving program subset;
5) verified by the software coverage strength rank required in DO-178B/C according to proving program subset; If be proved to be successful, then model to be verified is by checking;
If authentication failed, then model to be verified is not by checking;
Described coverage strength rank comprises statement judgement, the condition revised and judges to cover.
Above-mentioned verification msg maker, according to the definition of data type and constraint thereof, generates verification msg sample, comprises normal input and extremely inputs data; Set up the DEFINED BY EQUIVALENT CLASS of verification msg, adopt the method for accidental validation, boundary value analysis to generate verification msg collection;
Described verifying logic maker is according to characteristic model, and the constraint between interface and dependence, adopt the mode of combined authentication, generates the verification msg of various combination coverage rate, determine the verifying logic collection in proof procedure.
Above-mentioned proving program generates and Chooser comprises proving program information definition module, verification environment configuration module, proving program choose module;
The information input source of described proving program information definition module is the checking case masterplate of checking personnel manual configuration; Described masterplate uses XML text, described masterplate mainly comprises the total information of checking case in Verification Project, described proving program information definition module utilizes use-case masterplate, and authentication data set and verifying logic collection are assembled, and generates normal authentication use-case and abnormal checking case; According to the service precondition in feature services model, service postcondition and service constraints, according to dependence order and checking target, some checking cases are combined, generates proving program collection;
Described verification environment configuration module is used for the verification environment of configuration verification, and described verification environment comprises host model, target machine model, operating system configuration, memory configurations, various kit;
Described proving program is chosen module and is selected different proving program subsets according to the software level defined in described proving program collection and verification environment and DO-178B.
Above-mentioned data type modeling comprises dtd-data type definition module and data type constraints definition module;
Described dtd-data type definition module is used for defining simple types and describes, defines enumeration type description and definition structure body type specification;
Described data type constraints definition module is used for defining effective value and enumerates, defines length constraint and interval of definition constraint;
Described feature services modeling comprises service essential information definition module and service parameter information definition module;
Described service essential information definition module is used for defining service describing, definition service precondition, definition service postcondition and definition service constraints;
The described essential information of service parameter information definition module definition service parameter, the data pool of definition service parameter.
The invention has the advantages that:
1, the method that the present invention adopts not only defines DO-178B/C software standard to be needed to verify target call, and proposes the method for checking.
2, the software level that method of the present invention can define in DO-178B/C selects different proving program subsets, realizes the checking of different stage software in DO-178B/C.
Accompanying drawing explanation
accompanying drawing 1model verification method system flow
figure;
accompanying drawing 2the signal of model conversion device
figure;
accompanying drawing 3the signal of proving program generation and selector switch
figure;
accompanying drawing 4the signal of proving program administration module
figure;
Embodiment
Below in conjunction with
accompanying drawing 1provide the specific embodiment of the model verification method meeting DO-178B/C A level software:
The specific embodiments of each ingredient of this method is:
Step 1) build verification system framework;
Wherein, verification system framework comprises model conversion layer, verification msg and logic generation layer, proving program generates and chooses layer;
Specifically, the function of model conversion layer is: by model conversion device, input model is converted to several characteristic models; The transfer process of model conversion device is the process of data type modeling and feature services modeling; Say further, feature modeling resolves software model exactly, therefrom to extract between main data, interface and interface the principal characters such as dependence, sets up unified, irrelevant with concrete model characteristic model, and different forms language is described, so that machine automatic Understanding and process.The extraction of characteristic model and abstractdesription are the bases that proving program robotization generates.
as Fig. 2shown in: model conversion device can be subdivided into data type modeling and feature services modeling two modules.
Data type MBM can be subdivided into dtd-data type definition and data type constraints defines two modules.
The function that dtd-data type definition module completes is:
Definition simple types describes;
Definition enumeration type describes;
Definition structure body type specification;
The function that data type constraints definition module completes is:
Definition effective value is enumerated;
Definition length constraint;
Interval of definition retrains;
Wherein, effective value constraint is used for the constraint of arbitrary data types, and length constraint is used for the constraint of character string type, and Operations of Interva Constraint is used for the constraint of value type.
Feature services MBM can be subdivided into the definition of service essential information and service parameter information defines two modules.See
accompanying drawing 2.
The function that service essential information definition module completes is:
Definition service describing;
Definition service precondition;
Definition service postcondition;
Definition service constraints;
The function that service parameter information definition module completes is:
The essential information of definition service parameter;
The data pool of definition service parameter;
Specifically, the function of verification msg generation layer is: several characteristic modules are generated verification msg collection respectively by verification msg maker, generates verifying logic collection by verifying logic maker;
Say further, verification msg generation module can be subdivided into data pool model management and checking behavior description two modules.Verification msg maker, mainly according to the definition of data type and constraint thereof, generates verification msg sample, comprises normal input and extremely inputs data; Set up the DEFINED BY EQUIVALENT CLASS of verification msg, adopt the method such as accidental validation, boundary value analysis to generate verification msg collection.Verifying logic maker is feature based service model mainly, considers the constraint between interface and dependence, adopts the thought of combined authentication, generates the verification msg of various combination coverage rate, determines the verifying logic collection in proof procedure.
Specifically, the function of proving program generation and selection layer is: by proving program generation and selector switch, verification msg collection and verifying logic collection are generated as proving program collection;
as Fig. 3shown in, proving program generates and selector switch can be subdivided into proving program information definition, verification environment configures, proving program chooses three modules.。
The information input source of proving program information definition module is the checking case masterplate of checking personnel manual configuration.This masterplate can use XML text, the realization of the checking case of language-specific (such as C language) easy to use like this.This masterplate mainly comprises the total information of checking case in Verification Project, such as: knowledge
property right, version change, the information such as demand tracking.
Proving program information definition module, on the basis of configuration verification use-case masterplate, is assembled the concrete behavior of the data in data pool with checking behavior description, is generated normal authentication use-case and abnormal checking case; Again according to the service precondition in feature services model, service postcondition and service constraints, according to specific dependency order (such as: order performs or concurrence performance) and checking target, some checking cases are combined, generates the body matter of proving program.
Verification environment configuration module can automatically or by verification environment of certain checking of checking personnel manual configuration, such as: host model, target machine model, operating system configuration, memory configurations, various kits etc.
Step 2) user is by mode input to be verified in model conversion layer, and model to be verified is converted to several characteristic models by model conversion device; Wherein, model to be verified comprises Rhapsody model, simulink model and other models;
Step 3) input to verification msg and logic generation layer with several characteristic models and generate verification msg collection and verifying logic collection by verification msg maker and verifying logic maker;
Step 4) utilize proving program to generate and select the proving program generation in layer and selector switch that verification msg collection and verifying logic collection are generated proving program collection; Concentrate from proving program and select proving program subset;
Step 5) verified by the software coverage strength rank required in DO-178B/C according to proving program subset; If be proved to be successful, then model to be verified is by checking;
If authentication failed, then model to be verified is not by checking;
Wherein, coverage strength rank comprises statement judgement, the condition revised and judges to cover.
On the basis of proving program collection and verification environment, according to the software level defined in DO-178B/C (A, B and C level), adopt algorithms of different, select different proving program subsets.
In addition, need to further illustrate: adopt during the method and can adopt verification management module; For building the difficulty of checking running environment to reduce checking personnel, help checking personnel rapid build verification platform, numerous proving programs in a project or even multiple project are carried out to the management of systematization, stratification, be convenient to these assets of checking personnel efficient multiplexing.
as Fig. 4shown in: verification management module can be subdivided into operation configuration management and proving program manages two modules.
Operation configuration management can be subdivided into data set configuration management, running environment configuration management and target machine and manage three modules.
The function that data set Configuration Manager completes is:
Data set configures---and comprise data name and arrange and the setting of data set path;
Checking case root directory is arranged;
Proving program root directory is arranged;
The function that running environment Configuration Manager completes is:
The start address of configuration data memory block, code area;
The startup path of configuration purpose marking machine (if being suitable for);
The startup path of configuring virtual machine (if being suitable for);
The function that target machine administration module completes is:
Add target machine;
Modifying target machine information;
Delete target machine;
Automatically the proving program quantity generated due to modelling verification instrument may be comparatively large, some proving program under the particular requirement of a certain project may and inapplicable.Proving program administration module provides means for the maintenance of checking personnel to such proving program, comprising: proving program amendment, proving program are deleted and proving program browses three modules.
Claims (4)
1. meet a model verification method for DO-178B/C A level software, it is characterized in that, comprise the following steps:
1) verification system framework is built;
Described verification system framework comprises model conversion layer, verification msg and logic generation layer, proving program generates and chooses layer;
Input model is converted to several characteristic models by model conversion device by described model conversion layer; The transfer process of described model conversion device is the process of data type modeling and feature services modeling;
Several characteristic modules are generated verification msg collection respectively by verification msg maker by described verification msg generation layer, generate verifying logic collection by verifying logic maker;
Described proving program generates and select layer to be generated by proving program and verification msg collection and verifying logic collection are generated as proving program collection by selector switch;
2) user is by mode input to be verified in model conversion layer, and model to be verified is converted to several characteristic models by model conversion device;
3) input to verification msg and logic generation layer with several characteristic models and generate verification msg collection and verifying logic collection by verification msg maker and verifying logic maker;
4) utilize proving program to generate and select the proving program generation in layer and selector switch that verification msg collection and verifying logic collection are generated proving program collection; Concentrate from proving program and select proving program subset;
5) verified by the software coverage strength rank required in DO-178B/C according to proving program subset; If be proved to be successful, then model to be verified is by checking;
If authentication failed, then model to be verified is not by checking;
Described coverage strength rank comprises statement judgement, the condition revised and judges to cover.
2. the model verification method meeting DO-178B/C A level software according to claim 1, is characterized in that: described verification msg maker, according to the definition of data type and constraint thereof, generates verification msg sample, comprises normal input and extremely inputs data; Set up the DEFINED BY EQUIVALENT CLASS of verification msg, adopt the method for accidental validation, boundary value analysis to generate verification msg collection;
Described verifying logic maker is according to characteristic model, and the constraint between interface and dependence, adopt the mode of combined authentication, generates the verification msg of various combination coverage rate, determine the verifying logic collection in proof procedure.
3. the model verification method meeting DO-178B/C A level software according to claim 1, is characterized in that: described proving program generates and Chooser comprises proving program information definition module, verification environment configuration module, proving program choose module;
The information input source of described proving program information definition module is the checking case masterplate of checking personnel manual configuration; Described masterplate uses XML text, described masterplate mainly comprises the total information of checking case in Verification Project, described proving program information definition module utilizes use-case masterplate, and authentication data set and verifying logic collection are assembled, and generates normal authentication use-case and abnormal checking case; According to the service precondition in feature services model, service postcondition and service constraints, according to dependence order and checking target, some checking cases are combined, generates proving program collection;
Described verification environment configuration module is used for the verification environment of configuration verification, and described verification environment comprises host model, target machine model, operating system configuration, memory configurations, various kit;
Described proving program is chosen module and is selected different proving program subsets according to the software level defined in described proving program collection and verification environment and DO-178B.
4. the model verification method meeting DO-178B/C A level software according to claim 1, is characterized in that: described data type modeling comprises dtd-data type definition module and data type constraints definition module;
Described dtd-data type definition module is used for defining simple types and describes, defines enumeration type description and definition structure body type specification;
Described data type constraints definition module is used for defining effective value and enumerates, defines length constraint and interval of definition constraint;
Described feature services modeling comprises service essential information definition module and service parameter information definition module;
Described service essential information definition module is used for defining service describing, definition service precondition, definition service postcondition and definition service constraints;
The described essential information of service parameter information definition module definition service parameter, the data pool of definition service parameter.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201410728455.5A CN104461882B (en) | 2014-11-29 | 2014-11-29 | Method for model verification of software conforming to DO-178B/C A level |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN201410728455.5A CN104461882B (en) | 2014-11-29 | 2014-11-29 | Method for model verification of software conforming to DO-178B/C A level |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN104461882A true CN104461882A (en) | 2015-03-25 |
| CN104461882B CN104461882B (en) | 2017-05-17 |
Family
ID=52907971
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN201410728455.5A Active CN104461882B (en) | 2014-11-29 | 2014-11-29 | Method for model verification of software conforming to DO-178B/C A level |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN104461882B (en) |
Cited By (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN106528100A (en) * | 2015-08-05 | 2017-03-22 | 通用电气公司 | System and method for model based technology and process for safety-critical software development |
| CN111143212A (en) * | 2019-12-24 | 2020-05-12 | 中国航空工业集团公司西安飞机设计研究所 | A functional logic function library verification method under the modular integrated software architecture |
Citations (7)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US20100195634A1 (en) * | 2008-09-04 | 2010-08-05 | Thompson Aerospace | Method to provide connectivity and power for different aircraft sub-systems varying in levels of criticality and intended purposes while using a single partitioned Airborne Local Area Network (ALAN) |
| CN101986318A (en) * | 2010-11-26 | 2011-03-16 | 南京航空航天大学 | Design method of concept prototype of flight control system |
| CN103213677A (en) * | 2012-01-24 | 2013-07-24 | 空中客车运营简化股份公司 | A method and device for assisted piloting of an aircraft during a landing phase |
| TW201335575A (en) * | 2012-02-28 | 2013-09-01 | Vishay S A | Rotary position sensor device |
| CN103617115A (en) * | 2013-10-30 | 2014-03-05 | 北京信息控制研究所 | Runtime error analytical method based on abstract interpretation and model verification |
| CN103853871A (en) * | 2013-11-21 | 2014-06-11 | 北京航空航天大学 | Safety requirement modeling method applicable for avionics system |
| CN103970652A (en) * | 2014-04-29 | 2014-08-06 | 南京邮电大学 | Wireless sensor network software code verification method based on bounded model checking |
-
2014
- 2014-11-29 CN CN201410728455.5A patent/CN104461882B/en active Active
Patent Citations (7)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US20100195634A1 (en) * | 2008-09-04 | 2010-08-05 | Thompson Aerospace | Method to provide connectivity and power for different aircraft sub-systems varying in levels of criticality and intended purposes while using a single partitioned Airborne Local Area Network (ALAN) |
| CN101986318A (en) * | 2010-11-26 | 2011-03-16 | 南京航空航天大学 | Design method of concept prototype of flight control system |
| CN103213677A (en) * | 2012-01-24 | 2013-07-24 | 空中客车运营简化股份公司 | A method and device for assisted piloting of an aircraft during a landing phase |
| TW201335575A (en) * | 2012-02-28 | 2013-09-01 | Vishay S A | Rotary position sensor device |
| CN103617115A (en) * | 2013-10-30 | 2014-03-05 | 北京信息控制研究所 | Runtime error analytical method based on abstract interpretation and model verification |
| CN103853871A (en) * | 2013-11-21 | 2014-06-11 | 北京航空航天大学 | Safety requirement modeling method applicable for avionics system |
| CN103970652A (en) * | 2014-04-29 | 2014-08-06 | 南京邮电大学 | Wireless sensor network software code verification method based on bounded model checking |
Non-Patent Citations (1)
| Title |
|---|
| 陈世航: "《基于RTCADO_178B的软件独立测试验证的研究和实践》", 《中国优秀硕士学位论文全文数据库信息科技辑》 * |
Cited By (4)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| CN106528100A (en) * | 2015-08-05 | 2017-03-22 | 通用电气公司 | System and method for model based technology and process for safety-critical software development |
| CN106528100B (en) * | 2015-08-05 | 2020-06-09 | 通用电气公司 | System and method for model-based techniques and processes for safety-critical software development |
| CN111143212A (en) * | 2019-12-24 | 2020-05-12 | 中国航空工业集团公司西安飞机设计研究所 | A functional logic function library verification method under the modular integrated software architecture |
| CN111143212B (en) * | 2019-12-24 | 2023-06-23 | 中国航空工业集团公司西安飞机设计研究所 | Functional logic function library verification method under module integrated software architecture |
Also Published As
| Publication number | Publication date |
|---|---|
| CN104461882B (en) | 2017-05-17 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| CN106940428B (en) | Chip verification method, device and system | |
| US9754059B2 (en) | Graphical design verification environment generator | |
| US11182132B1 (en) | Determining functional equivalence of configurations of a model | |
| US9904524B2 (en) | Method and device for visually implementing software code | |
| CN114139475A (en) | Chip verification method, system, device and storage medium | |
| CN106598924A (en) | Form generation method and device | |
| CN104598240A (en) | Platform-spanning simulation model development method and system | |
| CN104090776A (en) | Software development method and system | |
| US20150135164A1 (en) | Integrated Software Testing Management | |
| CN102117449A (en) | Dynamic verification and soft handover method for online state entering of power grid model | |
| CN102147758A (en) | Automatic compiling and configuring method for equipment to be tested, device and system | |
| CN103123605A (en) | Android platform automation integration testing method and device | |
| CN106649112A (en) | Platform plug-in technology oriented testing method | |
| Xu et al. | Llm-aided efficient hardware design automation | |
| CN106484452B (en) | unified configuration management method and device for software platform | |
| CN104461882A (en) | Method for model verification of software conforming to DO-178B/C A level | |
| CN106383832A (en) | Data excavation training model forming method | |
| CN105843982A (en) | Bit stream generating method and device and design system used for programmable logic device | |
| CN108287788A (en) | A kind of use-case step matching method based on test case, system | |
| US20150355997A1 (en) | Server-Platform Simulation Service | |
| CN109710532A (en) | Test case management method and device and electronic equipment | |
| Quan et al. | IMA reconfiguration modeling and reliability analysis based on AADL | |
| CN104133680A (en) | Fast building method of ERP form module | |
| Moretti | Accellera’s Support for ESL Verification and Stimulus Reuse | |
| Sharma et al. | Quality assurance of component based software systems |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| C06 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |