http://dspace.nbuv.gov.ua:80/handle/123456789/1231 Tue, 07 Apr 2026 16:45:00 GMT 2026-04-07T16:45:00Z http://dspace.nbuv.gov.ua:80/bitstream/id/127210/ http://dspace.nbuv.gov.ua:80/handle/123456789/1231 http://dspace.nbuv.gov.ua:80/handle/123456789/1304 Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation Goerigk, Wolfgang; Langmaack, Hans The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorrectness of ystems, will they be able to justify systems to work correctly as intended? We understand the word justification in this sense, i.e. for the design of computer based systems, the formulation of mathematical models of information flows, and the construction of controlling software to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation — bootstrapping — of high level compiler programs into host machine code by existing host ompilers, is as important. So far there are no realistic recipes to close this gap, although it is known for many years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori code inspection, which has been developed by the research group Verifix funded by the Deutsche Forschungsgemeinschaft (DFG).; Багато років теоретична інформатика вчастині розробки програмного забезпечення і побудови компіляторів займалась проблемами правильності специфікацій і високорівневих реалізацій компіляторів. У другій частині статті розглядається проблема коректного і безпечного перекладу (bootstrapping) програм з мови високого рівня в коди машини. Показано, як вирішуються проблеми коректності програм на мовах низького рівня. Продемонстрований метод строго синтаксичного апостеріор ного аналізу, котрий був розроблений дослідною групою Verifix в університеті м. Киля (ФРН).; Много лет теоретическая информатика в части разработки программного обеспечения и построения компиляторов занималась проблемами правильности спецификаций и высокоуровневых реализаций компиляторов. Во второй части статьи рассматривается проблема корректного и безопасного перевода (bootstrapping) программ с языка высокого уровня в коды машины. Показано, как решаются проблемы корректности программ на языках низкого уровня. Продемонстрирован метод строго синтаксического апостериорного анализа, который был разработан исследовательской группой Verifix в университете г. Киля (ФРГ). Wed, 01 Jan 2003 00:00:00 GMT http://dspace.nbuv.gov.ua:80/handle/123456789/1304 2003-01-01T00:00:00Z http://dspace.nbuv.gov.ua:80/handle/123456789/1302 Формальные модели компонентного программирования Грищенко, В.Н. Предложен подход к построению формальных моделей компонентного программирования как основы создания компонентной теории. Рассмотрены модели компонентов, компонентных сред, определены внешняя и внутренняя компонентные алгебры. Проанализированы различные аспекты предложенных моделей и их связь с практикой программирования.; Запропоновано підхід до побудови формальних моделей компонентного програмування як основи створення компонентної теорії. Розглянуті моделі компонентів і компонентних середовищ, визначені зовнішня та внутрішня компонентні алгебри. Проаналізовані різні аспекти запропонованих моделей і їх зв’язок з практикою програмування.; The approach to construction of formal models of component programming, as bases of component theory creation, is offered. The models of components, component environments and external and internal component algebra are considered. The various aspects of these models and their relations with practice of programming are analysed. Wed, 01 Jan 2003 00:00:00 GMT http://dspace.nbuv.gov.ua:80/handle/123456789/1302 2003-01-01T00:00:00Z http://dspace.nbuv.gov.ua:80/handle/123456789/1296 Концепція керiваного проектування інформаційних систем управлінської діяльності Задорожна, Н.Т.; Валь, К.Л. Аналізується процес проектування інформаційних систем (ІС) управлінської діяльності. Пропонуються нові принципи моделювання задач керування технологічним процесом проектування, контролю та корекції плану робіт зі створення ІС. Визначена формальна модель керування проектуванням таких систем. Наведено приклад її застосування.; Анализируется процесс проектирования информационных систем управленческой деятельности. Предлагаются новые принципы моделирования задач управления технологическим процессом проектирования, контроля и корректировки плана работ. Определена формальная модель управления проектированием информационных систем. Приведен пример ее применения.; The information systems project management process to support for Government bodies is analysed. New principles of project management technological process model, control and correction of working plans are suggested. The formal model of information systems project management is defined. The example using of this model is represented. Wed, 01 Jan 2003 00:00:00 GMT http://dspace.nbuv.gov.ua:80/handle/123456789/1296 2003-01-01T00:00:00Z http://dspace.nbuv.gov.ua:80/handle/123456789/1294 Синтез автомата, специфицированного множеством дизъюнктов Чеботарев, А.Н. Предложен подход к синтезу автомата, специфицированного логической формулой в конъюнктивной нормальной форме (к.н.ф.). Хотя при этом используется метод синтеза автомата по формуле, представленной в дизъюнктивной нормальной форме (д.н.ф.), при синтезе не требуется преобразование к.н.ф. в д.н.ф. Благодаря этому предложенный метод имеет ту же эффективность, что и метод, на котором он основан.; Запропоновано підхід до синтезу автомата, який специфіковано логічною формулою у кон’юнктивній нормальній формі (к.н.ф.). Хоча при цьому використовується метод синтезу автомата за специфікацією, яку подано у диз’юнктивній нормальній формі (д.н.ф.), синтез виконується без перетворення к.н.ф. у д.н.ф. Завдяки цьому запропонований метод має ту ж саму ефективність, що й метод, на якому він базується.; An approach to synthesis of an automaton specified by the logical formula in the conjunctive normal form (c.n.f.) is proposed. Although this approach exploits the method for synthesis of an automaton from the specification represented in the disjunctive normal form (d.n.f.), the synthesis is carried out without transforming c.n.f. into d.n.f. Owing to this fact the proposed method has the same efficiency as the method at which it is based. Wed, 01 Jan 2003 00:00:00 GMT http://dspace.nbuv.gov.ua:80/handle/123456789/1294 2003-01-01T00:00:00Z