O.S.E.L. - Sbohem, poruchové počítačové programy!
 Sbohem, poruchové počítačové programy!
Bude někdy možné, abyste si koupili počítačový program s garancí, že je bez chyb? Tým evropských vědců se domnívá, že ano. Jejich práce na matematických základech programování by mohla být revolucí v softwarovém průmyslu.


 

Začínáme si „nebezpečně“ zvykat na myšlenku, že počítačový program nemusí vždy pracovat správně. Zatímco poruchové auto vrátíme zpátky prodejci a požadujeme nápravu, v otázce poruchovosti počítačových programů jsme pozoruhodně tolerantní.

Program, který kupujeme, je obvykle bez záruky a nechvalně známé „zřeknutí se odpovědnosti“ je všechny provází, jako nedílná součást instalačního manuálu. Snad už ani nikdo neočekává, že všechno bude fungovat správně, jakmile se to jednou vybalí „z krabice“. A co je snad nejhorší, neočekává to ani sám výrobce. Ve skutečnosti to většinou vypadá tak, že firmy vyvíjející a prodávající software spoléhají na to, že jejich zákazníci objeví chyby, které pak mohou „zalepit“ vydáním „upgradu“ produktu.

 

 
Bengt Nordström, počítačový odborník na Chalmers University v Göteborgu: „Softwarový průmysl je stále velmi „nevyspělý“, alespoň ve srovnání s ostatními odvětvími technických oborů. Chceme brát programování jako technický vědní obor, ale zatím to tak nevypadá. Nezakládá se na dobré teorii, ani nemáme dobrou metodu výpočtu k tomu, abychom se mohli ujistit, že v každém kroku vyrobíme něco, co je správně.“


 
Nordström si myslí, že celý přístup k psaní programů by měl být přehodnocen. Obvyklý přístup spočívá v ověření správnosti fungování programu prostřednictvím dlouhého testovacího procesu. Namísto toho bychom rádi viděli návrh základního principu, který zaručí, že od „první věty“ bude program opravdu dělat to, co se od něj očekává a co je napsáno na krabici v které ho koupíte.
Klíč k tomuto problému leží v těžko srozumitelných matematických formulacích, které popisuje takzvaná „teorie modelu“ založená na teorii výpočtu. V tomto přístupu je specifikace pro výpočetní úlohu uvedená jako matematický teorém. Program, který provádí výpočet, je obdobou prokázání teorému. Ověřením tohoto teorému je zaručeno, že program bude v pořádku.

 

Otevřený zdrojový kód programu
Samozřejmě, že to není tak jednoduché, ale teorie modelu je tak slibnou možností, že Evropská unie již od roku 1989 financuje celý řetězec projektů k jejímu vývoji, pod záštitou programu Future and Emerging Technologies.
Nordström byl koordinátorem jednoho z projektů, nazvaného TYPES, který podporoval spolupráci výzkumníků zabývajících se touto problematikou na 15 evropských univerzitách a výzkumných ústavech společně s těmi v 19 vědeckých a průmyslových organizacích.
Partneři projektu TYPES také vydávají otevřené zdrojové programové balíky, které si může kdokoliv stáhnout, použít a upravit. Tyto balíky obsahují několik „testovacích editorů“, které jsou v teorii modelu klíčem k zaručení správnosti programů.

Může takový abstraktní teoretický výzkum opravdu vést k bezporuchovému softwaru?

„Evropský výzkum v této oblasti je nejsilnějším na světě,“ zdůrazňuje Nordström. „Mnoho počítačových programů pracuje špatně nebo nepracuje odpovídajícím způsobem a v dlouhodobém časovém horizontu může být tento výzkum skutečně významným pomocníkem. Jde o velmi pomalý proces a zabere to spoustu let, než dostaneme tento nápad z univerzit do „provozu“, ale myslím si, že už si zde pomalu nachází své místo.“

 
„Princip otevřeného zdroje je nezbytný pro to, čeho se pokoušíme dosáhnout,“ říká Nordström. „Je důležité, aby kdokoliv mohl vyhodnotit tento zdrojový kód a zkontrolovat, jestli je správný. Takže neodmyslitelnou součástí tohoto projektu by mělo být, že cokoliv v programu uděláme, bude přístupné i ostatním, aby se o tom mohlo následně diskutovat.“
Výsledky z teorie modelu si již našly svou cestu do jiných projektů. Příkladem může být projekt Moebius, financovaný Evropskou unií, který vyvíjí nové metody, tak zvané „testovací kódy“, jejichž účelem bude ověřovat bezchybnost stahovatelných programů.
Jedna francouzská společnost využívá myšlenky z teorie modelu k návrhům napevno nainstalovaných počítačových programů, jaké jsou například používané v „chytrých kartách“. A ani Japonsko nezůstává v této oblasti výzkumu pozadu.

 

Zvětšit obrázek
Když selže software, přicházejí na pomoc některé hardwarové pomůcky vedoucí k restartu, kterým většina lidí problémy s takovým trucujícím programem řeší. Vždyť také jednou z prvních otázek pracovníků „hot-line“ bývá: „A zkoušeli jste to restartovat?“

Teorie v praxi
Výzkumníci také předvedli schopnosti teorie modelu prověřením klasického teorému „čtyř barev“ jedním z testovacích editorů používáných v projektu TYPES. Ale teorie modelu také nachází uplatnění i v jazykových analýzách.
Nordström se nedomnívá, že by využití teorie modelu bylo nezbytné pro všechny programy, ale je zcela jasné, že bude potřeba například pro zabezpečení rozhodujících bankovních systémů. Krom toho by teorie modelu mohla být důležitou též v oblastech dopravy, obrany a zdravotnictví, kde může být za chyby v programech placeno lidskými životy.

 

TYPES obdržel finance od Evropské unie z programu Sixth Framework Programme pro výzkum spočívající v „koordinační činnosti“ popisující projekty, jejichž cílem je spíš „promazávat soukolí“ spolupráce, než přímo vyvíjet novou technologii. TYPES spojuje základní a aplikovaný výzkum. „To je jedna z věcí, kterou na této práci shledávám velmi zajímavou v porovnání s ostatními vědními obory,“ poznamenává Nordström. „Je nás celkem asi 150 lidí, kteří pracují na tomto projektu a je to směsice velmi praktických osob s velmi teoreticky orientovanými lidmi a mnoho si toho vzájemně poskytujeme. Myslím si, že je to velmi vzácné v porovnání s ostatními vědeckými projekty.“

 

Nordström doufá, že tato práce vykonaná v rámci projektu TYPES konečně umožní programování „dozrát“ do skutečně technické disciplíny se stejně vysokými standardy a zárukou kvality, jakou nyní očekáváme v kterémkoliv jiném technickém oboru.
„Mnoho úsilí je nyní věnováno testování softwaru,“ říká. „Velmi často jsou programy napsány ve spěchu, a pak jsou testovány a opravovány… a opět testovány a opravovány… a tak pořád dokola. To je strašně nesystematické. Není to ani vzdáleně podobné tomu, jak na příklad budujeme mosty a dálnice. Tento způsob práce nás připravuje na změnu tak, abychom více úsilí věnovali vlastnímu psaní programů, než jejich testování a opravování.“

Zdroj: ICT Results

 

fatal error


Autor: Ota Beran
Datum:23.07.2008 18:16