Формалды бағдарламалау спецификациялары

Кіріспе

Математикалық бағдарламалардың сипаттамалары

Компьютерлік ғылымда формальды әдістер – бағдарламалық және аппараттық жүйелерді нақтылау, жасау, талдау және тексеру үшін математикалық тұрғыдан қатаң әдістер. Бағдарламалық және аппараттық құрылымдауда формальды әдістерді қолдану себебі – басқа инженерлік салаларындағыдай, тиісті математикалық талдау жүргізу құрылымның сенімділігі мен тұрақтылығын арттыруға көмектеседі деген болжам. Формальды әдістер теориялық компьютерлік ғылымның түрлі негіздерін пайдаланады, олардың ішінде логикалық есептеулер, формальды тілдер, автоматтар теориясы, басқару теориясы, бағдарлама семантикасы, типтік жүйелер және типтік теория бар.

Өмірбаян

Жартылай ресми әдістер – толыққанды "формальды" деп есептелмейтін формализмдер мен тілдер. Олар семантиканы толықтыру міндетін кейінгі кезеңге ықпалдастырады, одан кейін бұл жұмыс адамның түсіндіруі немесе кодты немесе тест жағдайларын жасау сияқты бағдарламалық құралдар арқылы түсіндіру арқылы жүзеге асырылады.

Жеңіл формальды әдістер

Кейбір мамандар ресми әдістер қауымдастығы спецификацияны немесе жобаны толық ресімдеуге артық көңіл бөлді деп есептейді. Олардың пікірінше, қолданылатын тілдердің мүмкіндіктері, сондай-ақ модельделетін жүйелердің күрделілігі толық ресімдеуді қиын және қымбат міндет етеді. Оның орнына, ішінара сипаттамаға және нақты қолдануға баса назар аударатын түрлі жеңілдетілген ресми әдістер ұсынылған. Формальды әдістерге жеңіл тәсілдің мысалдарына Alloy нысандық модельдеу нотациясы, Denney-дің Z нотациясының кейбір аспектілерін қолдану жағдайларына негізделген әзірлемемен және CSK VDM құралдарымен біріктіруі жатады.

Қолданылуы

Ресми әдістерді даму процесінің әртүрлі сатыларында қолдануға болады.

Ерекшеліктер

Қажетті егжей-тегжейлілік деңгейіне қарамастан, дамытылатын жүйені сипаттау үшін формалды әдістер қолданылуы мүмкін. Бұл формалды сипаттама одан әрі даму шараларын басқару үшін пайдаланылуы мүмкін (кейінгі бөлімдерді қараңыз); сондай-ақ, дамытылып жатқан жүйеге қойылатын талаптардың толық және нақты көрсетілгенін тексеруге немесе оларды нақты және бірмәнді анықталған синтаксис және семантикасы бар формалды тілде жазу арқылы жүйе талаптарын формалдауға қолданылуы мүмкін. Формалды спецификация жүйелерінің қажеттілігі көп жылдар бойы айтылып келеді. ALGOL 58 есебінде Джон Бэкус бағдарламалау тілінің синтаксисін сипаттау үшін формалды нотация ұсынды, кейіннен ол Backus қалыпты түрі деп, содан кейін Backus-Naur түрі (BNF) деп аталды. Бэкус сонымен қатар синтаксистік тұрғыдан дұрыс ALGOL бағдарламаларының мағынасын формалды түрде сипаттау есепке енгізу үшін уақытында аяқталмағанын жазды. "Сондықтан заңды бағдарламалардың семантикасын формалды қарастыру келесі мақалада жарияланады". Бірақ ол жарияланбады.

Даму

Ресми әзірлеу – құралдармен қолдау көрсетілетін жүйелерді әзірлеу процесінің бір бөлігі ретінде формальды әдістерді пайдалану. Формальды сипаттама жасалғаннан кейін, ол жобалау кезінде нақты жүйе құрылғанда (әдетте бағдарламалық қамтамасыз етуде, бірақ аппараттық құралдарда да мүмкін) нұсқаулық ретінде қолданылуы мүмкін. Мысалы:

Егер формальды сипаттама операциялық семантикада жазылған болса, нақты жүйенің көрінетін әрекеттері сипаттаманың әрекеттерімен салыстырылуы мүмкін (өзі орындалатын немесе модельдеуге болатын). Сонымен қатар, сипаттаманың операциялық командаларын орындалатын кодқа тікелей аударуға болады. Егер формальды сипаттама аксиоматикалық семантикада жазылған болса, сипаттаманың алғы және кейінгі шарттары орындалатын кодтағы тексерулерге айналуы мүмкін.

Тексеру

Ресми тексеру – бұл бағдарламалық құралдарды ресми сипаттаманың қасиеттерін дәлелдеу үшін немесе жүйе іске асыруының ресми моделі оның сипаттамасына сәйкес екенін дәлелдеу үшін қолдану. Ресми сипаттама жасалғаннан кейін, оны сипаттаманың қасиеттерін, ал одан шығарылған нәрсе арқылы жүйе іске асыруының қасиеттерін дәлелдеу үшін негіз ретінде пайдалануға болады.

Қолтаңбалауды тексеру

Тексеруді бекіту – жоғары деңгейде сенімді ресми тексеру құралын қолдану. Мұндай құрал дәстүрлі тексеру әдістерінің орнына келе алады (құрал тіпті сертификатталған болуы мүмкін).

Адамның басқаруымен дәлелдеу

Кейде жүйенің дұрыстығын дәлелдеуге түрткіс жүйенің дұрыстығына көз жеткізу қажеттілігі емес, жүйені жақсырақ түсіну ниеті болуы мүмкін. Осының салдарынан, кейбір дұрыстық дәлелдемелері математикалық дәлелдеу стилінде жасалады: қолмен жазылған (немесе жинақталған), табиғи тілді қолдана отырып, мұндай дәлелдемелерге тән бейресмилік деңгейін сақтайды. "Жақсы" дәлел – басқа адамдар оқи және түсіне алатын дәлел. Мұндай тәсілдерді сынаушылар табиғи тілге тән екіұштылықтың осындай дәлелдемелерде қателерді байқаусыз қалдыруға мүмкіндік беретінін атап көрсетеді; көбінесе, мұндай дәлелдемелерде әдетте назардан тыс қалдырылатын төменгі деңгейдегі ұсақ-түйектерде елеусіз қателер кездесуі мүмкін. Бұған қоса, мұндай жақсы дәлелді жасау математикалық білім мен тәжірибеліліктің жоғары деңгейін талап етеді.

Автоматтандырылған дәлелдеу

Керісінше, мұндай жүйелердің дұрыстығын автоматтандырылған тәсілдермен дәлелдеуге қызығушылық артып келеді. Автоматтандырылған техникалар үш негізгі санатқа бөлінеді: Автоматтандырылған теоремаларды дәлелдеу, онда жүйе жүйе сипаттамасын, логикалық аксиомалар жиынтығын және логикалық қорыту ережелерінің жиынтығын пайдалана отырып, бастапқыдан ресми дәлелдеме жасауға тырысады. Модельді тексеру, онда жүйе орындалу барысында жүйеге түсе алатын барлық мүмкін күйлерді толық қарау арқылы белгілі бір қасиеттерді тексеріп шығады. Абстрактілік интерпретация, онда жүйе бағдарламаның мінез-құлқының шамадан тыс жуықтауын тексеру үшін оны көрсететін (толық болуы мүмкін) тордағы бекітілген нүкте есебін қолданады. Кейбір автоматтандырылған теоремаларды дәлелдейтін жүйелерге қай қасиеттерді іздеу "қызықты" екенін көрсету қажет, ал басқалары адамның араласуынсыз жұмыс істейді. Модельді тексерушілер жеткілікті абстрактілі модель берілмесе, миллиондаған пайдасыз күйлерді тексеруде тез тоқырап қалуы мүмкін. Мұндай жүйелерді қолдайтындар нәтижелердің адам жасаған дәлелдемелерге қарағанда математикалық тұрғыдан сенімдірек екенін айтады, себебі барлық егжей-тегжейлі мәліметтер алгоритмдік түрде тексерілген. Мұндай жүйелерді пайдалану үшін қажетті білім математикалық дәлелдемелерді қолмен жасау үшін қажетті білімнен кем, бұл техникаларды көптеген мамандарға қолжетімді етеді. Сынаушылар бұл жүйелердің кейбіреулері оракулдарға ұқсайтынын атап көрсетеді: олар шындықты айтады, бірақ оның себебін түсіндірмейді. Сондай-ақ "тексерушіні тексеру" мәселесі де бар; егер тексеруге көмектесетін бағдарламаның өзі дәлелденбесе, алынған нәтижелердің дұрыстығына күмән тудыруға болады. Кейбір қазіргі заманғы модельді тексеру құралдары дәлелдеменің әр қадамын егжей-тегжейлі көрсететін "дәлелдеме журналын" жасайды, бұл тиісті құралдар болған жағдайда тәуелсіз тексеруді жүргізуге мүмкіндік береді. Абстрактілік интерпретация тәсілінің басты ерекшелігі – ол дұрыс талдауды қамтамасыз етеді, яғни жалған теріс нәтижелер қайтарылмайды. Сонымен қатар, ол талданатын қасиетті көрсететін абстрактілік доменді реттеу арқылы және жылдам конвергенцияға қол жеткізу үшін кеңейту операторларын қолдану арқылы тиімді түрде кеңейтіледі.

In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:
Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules. Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. Abstract interpretation, in which a system verifies an over approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) lattice representing it. Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model. Proponents of such systems argue that the results have greater mathematical certainty than human produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners. Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification. The main feature of the abstract interpretation approach is that it provides a sound analysis, i. e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators to get fast convergence.

Қолданбалар

Формалды әдістер аппараттық және бағдарламалық қамтамасыз етудің әртүрлі салаларында қолданылады, соның ішінде маршрутизаторлар, Ethernet коммутаторлары, маршрутизациялық протоколдар, қауіпсіздік қолданбалары және seL4 сияқты операциялық жүйелердің микроядролары. Деректер орталықтарында қолданылатын аппараттық және бағдарламалық қамтамасыз етудің жұмыс істеуін тексеру үшін оларды қолданған бірнеше мысал бар. IBM, AMD x86 процессорларын әзірлеу процесінде ACL2 теореманы дәлелдейтін құралды қолданды. Intel өзінің аппараттық және микрокодтық бағдарламаларын (тек оқуға арналған жадқа бағдарламаланған тұрақты бағдарламалық қамтамасыз ету) тексеру үшін мұндай әдістерді пайдаланады. Dansk Datamatik Center 1980-ші жылдары Ada бағдарламалау тілі үшін компилятор жүйесін жасау үшін формалды әдістерді қолданды, ол ұзақ өмір сүрген коммерциялық өнімге айналды. NASA-ның бірнеше басқа да жобаларында формалды әдістер қолданылады, мысалы, Келесі буын әуе көлігі жүйесі, Ұлттық әуе кеңістігі жүйесіндегі ұшқышсыз ұшақ жүйесін интеграциялау және Әуедегі үйлестірілген қақтығыстарды шешу және анықтау (ACCoRD). B әдісі Atelier B-мен бірге Alstom және Siemens компаниялары бүкіл әлемде орнатылған әртүрлі метрополитендер үшін қауіпсіздік автоматикасын әзірлеуде, сондай-ақ ATMEL және STMicroelectronics компаниялары үшін жалпы критерийлерді сертификаттау және жүйелік модельдерді әзірлеуде қолданылады. Формалды тексеруді IBM, Intel және AMD сияқты көптеген танымал аппараттық өндірушілер аппараттық құралдарда жиі қолданады. Intel өнімдерінің жұмыс істеуін тексеру үшін формалды әдістерді қолданған көптеген аппараттық салалар бар, мысалы, кэш сәйкестігі протоколының параметрленген тексеруі, Intel Core i7 процессорларының орындалу механизмін растау (теоремаларды дәлелдеу, BDD және символдық бағалау), HOL light теореманы дәлелдейтін құралды қолдана отырып Intel IA 64 архитектурасын оңтайландыру және PCI Express протоколын қолдайтын жоғары өнімді екі портты гигабит Ethernet контроллерін тексеру, сондай-ақ Cadence пайдалану арқылы Intel алдын ала басқару технологиясы. Сол сияқты, IBM Power7 микропроцессорларының қуаттық шлюздерін, регистрлерін және функционалдық тексеруде формалды әдістерді қолданды.

Formal methods are applied in different areas of hardware and software, including routers, Ethernet switches, routing protocols, security applications, and operating system microkernels such as seL4. There are several examples in which they have been used to verify the functionality of the hardware and software used in data centres. IBM used ACL2, a theorem prover, in the AMD x86 processor development process. Intel uses such methods to verify its hardware and firmware (permanent software programmed into a read only memory). Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long lived commercial product. There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System, Unmanned Aircraft System integration in National Airspace System, and Airborne Coordinated Conflict Resolution and Detection (ACCoRD). B Method with Atelier B, is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics. Formal verification has been frequently used in hardware by most of the well known hardware vendors, such as IBM, Intel, and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache coherent protocol, Intel Core i7 processor execution engine validation (using theorem proving, BDDs, and symbolic evaluation), optimization for Intel IA 64 architecture using HOL light theorem prover, and verification of high performance dual port gigabit Ethernet controller with support for PCI express protocol and Intel advance management technology using Cadence. Similarly, IBM has used formal methods in the verification of power gates, registers, and functional verification of the IBM Power7 microprocessor.

Бағдарламалық жасақтауда

Бағдарламалық жасақтаманы әзірлеуде формалды әдістер – бағдарламалық (және аппараттық) жүйелердегі мәселелерді талаптар, сипаттама және жобалау деңгейінде шешуге арналған математикалық тәсілдер. Формалды әдістер, әсіресе қауіпсіздік пен қауіпсіздікке сезімтал бағдарламалық жасақтама мен жүйелерде, мысалы авиациялық бағдарламалық жасақтамада қолданылады. Бағдарламалық жасақтаманың қауіпсіздігін қамтамасыз ету стандарттары, мысалы DO 178C, қосымша материалдар арқылы формалды әдістерді пайдалануға рұқсат береді, ал Common Criteria ең жоғары санатта формалды әдістерді міндеттейді. Реттік бағдарламалық жасақтама үшін формалды әдістердің мысалдары: B әдісі, автоматты теореманы дәлелдеуде қолданылатын сипаттама тілдері, RAISE және Z нотациясы. Функционалдық бағдарламалауда қасиетке негізделген тестілеу жеке функциялардың күтілетін мінез-құлқының математикалық сипаттамасын жасауға және тестілеуге (толыққанды тестілеу болмаса да) мүмкіндік береді. Объектілік шектеу тілі (және Java модельдеу тілі сияқты маманданулар) объектіге бағытталған жүйелерді формалды түрде сипаттауға мүмкіндік береді, бірақ міндетті түрде формалды тексеруді қамтамасыз етпейді. Параллель бағдарламалық жасақтама мен жүйелер үшін Петри желілері, процесс алгебрасы және шекті күй машиналары (автоматтар теориясына негізделген; сондай-ақ виртуалды шекті күй машинасы немесе оқиға басқарылатын шекті күй машинасы қараңыз) орындалатын бағдарламалық жасақтаманың сипаттамасын жасауға және қолданба мінез-құлқын құру мен тексеруге мүмкіндік береді. Бағдарламалық жасақтаманы әзірлеудегі формалды әдістердің тағы бір тәсілі – спецификацияны логиканың қандай да бір түрінде – әдетте бірінші реттік логиканың нұсқасы – жазу және содан кейін логиканы бағдарлама сияқты тікелей орындау. Сипаттамалық логикаға негізделген OWL тілі осыған мысал. Сондай-ақ, ағылшын тілінің (немесе басқа табиғи тілдің) кейбір нұсқаларын логикаға автоматты түрде түрлендіру және логиканы тікелей орындау бойынша жұмыстар жүргізілуде. Мысалдар: Attempto Controlled English және Internet Business Logic, олар сөздік пен синтаксисті басқаруға тырыспайды. Екі бағытты ағылшын-логикалық түрлендіруді және логиканы тікелей орындауды қолдайтын жүйелердің ерекшелігі – олар өз нәтижелерін ағылшын тілінде, бизнес немесе ғылыми деңгейде түсіндіре алады.

In software development, formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety critical or security critical software and systems, such as avionics software. Software safety assurance standards, such as DO 178C allows the usage of formal methods through supplementation, and Common Criteria mandates formal methods at the highest levels of categorization. For sequential software, examples of formal methods include the B Method, the specification languages used in automated theorem proving, RAISE, and the Z notation. In functional programming, property based testing has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions. The Object Constraint Language (and specializations such as Java Modeling Language) has allowed object oriented systems to be formally specified, if not necessarily formally verified. For concurrent software and systems, Petri nets, process algebra, and finite state machines (which are based on automata theory; see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behaviour. Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of first order logic—and then to directly execute the logic as though it were a program. The OWL language, based on description logic, is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are Attempto Controlled English, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.

Ресми әдістер мен белгілер

Формалды әдістер мен нотациялардың түрлі нұсқалары қол жетімді.

Шешушілер мен байқаулар

Формальды әдістердегі көптеген мәселелер NP қиын, бірақ практикада кездесетін жағдайларда оларды шешуге болады. Мысалы, бульдік қанағаттандыру мәселесі Кук-Левин теоремасы бойынша NP-толық, бірақ SAT шешушілер әртүрлі үлкен мысалдарды шеше алады. Формальды әдістерде туындайтын әртүрлі мәселелер үшін "шешушілер" бар, және мұндай мәселелерді шешудегі соңғы жетістіктерді бағалау үшін көптеген жыл сайынғы жарыстар өткізіледі. SAT жарысы – бұл SAT шешушілерді салыстыратын жыл сайынғы байқау. SAT шешушілер Alloy сияқты формальды әдістер құралдарында қолданылады. CASC – теоремаларды автоматты түрде дәлелдейтін құралдардың жыл сайынғы жарысы. SMT COMP – формальды тексеруде қолданылатын SMT шешушілердің жыл сайынғы жарысы. CHC COMP – формальды тексеруге қолданылатын шектеулі Хорн шарттарын шешушілердің жыл сайынғы жарысы. QBFEVAL – модельдік тексеруге қолданылатын шындыққа квантталған бульдік формулаларды шешушілердің екі жылдық жарысы. SV COMP – бағдарламалық құралдарды тексеру құралдары үшін жыл сайынғы жарыс. SyGuS COMP – бағдарламалық синтез құралдарын жасау бойынша жыл сайынғы жарыс.