PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 5

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  software verification
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Efficiency of Software Testing Techniques: A Controlled Experiment Replication and Network Meta-analysis
Gómez O. S., Cortés-Verdín K., Pardo C. J.
e-Informatica Software Engineering Journal
|
2017
|
Vol. 11, nr 1
77--102
EN
Background. Common approaches to software verification include static testing techniques, such as code reading, and dynamic testing techniques, such as black-box and white-box testing. Objective. With the aim of gaining a better understanding of software testing techniques, a controlled experiment replication and the synthesis of previous experiments which examine the efficiency of code reading, black-box and white-box testing techniques were conducted. Method. The replication reported here is composed of four experiments in which instrumented programs were used. Participants randomly applied one of the techniques to one of the instrumented programs. The outcomes were synthesized with seven experiments using the method of network meta-analysis (NMA). Results. No significant differences in the efficiency of the techniques were observed. However, it was discovered the instrumented programs had a significant effect on the efficiency. The NMA results suggest that the black-box and white-box techniques behave alike; and the efficiency of code reading seems to be sensitive to other factors. Conclusion. Taking into account these findings, the Authors suggest that prior to carrying out software verification activities, software engineers should have a clear understanding of the software product to be verified; they can apply either black-box or white-box testing techniques as they yield similar defect detection rates.
2
Specification and verification of simple logic control programs using Frama C
Sadolewski J., Świder Z.
Studia Informatica
|
2011
|
Vol. 32, nr 3B
21-34
EN
The paper presents an approach to verification process for programs of simple logic controls written in ANSI C. The software is verified with open source tools like Frama C, Jessie and Coq. Process of specification determination and verification whether implementation conforms with specification is demonstrated by several examples, involving combinatorial logic, sequential logic and sequential logic with time constraints.
PL
W artykule zaproponowano proces weryfikacji prostych programów sterowania logicznego napisanych w ANSI C. Programy są weryfikowane przez ogólnodostępne narzędzia, jak Frama C, Jessie i Coq. Proces określania specyfikacji i weryfikacji zgodności specyfikacji z implementacją przedstawiono na kilku przykładach układów kombinacyjnych, sekwencyjnych oraz sekwencyjnych z uzależnieniami czasowymi.
3
Content available A safe programmable electronic system
Halang W., Śnieżek M.
Bulletin of the Polish Academy of Sciences. Technical Sciences
|
2010
|
Vol. 58, nr 3
423-434
EN
A dual-channel computer architecture for utilisation in programmable logic controllers is presented. Faults can be detected by novel high-speed comparators with fail-safe operation. The cyclic operating mode of PLCs and a specification-level, graphical programming paradigm based on the interconnection of application-oriented standard software function modules are architecturally supported. Thus, by design, there is no semantic gap between the programming and machine execution levels enabling the safety licensing of application software by an extremely simple, but rigorous method, viz., diverse back translation.
4
Content available Zastosowanie języka LOTOS do modelowania wybranych struktur metody HOOD
Brzuchcz R.
Elektrotechnika i Elektronika
|
2006
|
T. 25, z. 1
1-9
PL
W pracy zaprezentowano możliwości użycia języka LOTOS [3, 7] w projektowaniu oprogramowania systemów czasu rzeczywistego metodą HOOD [6, 13]. Wybrane struktury HOOD zostają wyrażone w języku algebry procesów i abstrakcyjnych typów danych, co zapewnia możliwość formalnej analizy tworzonego projektu. We wprowadzeniu do pracy wyjaśniono cel i motywacje do tworzenia modelu formalnego projektu systemu czasu rzeczywistego. Następnie przedstawiono skrócony opis metodyki hierarchicznego projektowania HOOD, której notacja i proces projektowy stanowią bazę dla proponowanej metody formalizacji. Wyjaśniono znaczenie takich konstrukcji, jak moduł, interfejs, operacja, hierarchia użycia i zawierania. W kolejnym punkcie, po krótkim przedstawieniu języka LOTOS [3, 7], zaprezentowano technikę, w której konstrukcje metody HOOD zostają zinterpretowane w języku formalnym algebry procesów i abstrakcyjnych typów danych. Opis przeprowadzony jest dla prostego przykładu projektu w HOOD, celem wyjaśnienia istoty interpretacji. W części końcowej pracy podano wnioski wraz ze wskazaniem dalszych możliwych kierunków rozwoju i zastosowań prezentowanej metody.
EN
The article presents a possibility of using LOTOS [3, 7] formal language in the HOOD [6, 13] real-time system design. Process algebras and abstract data types are used to express some HOOD structures in order to allow formal analysis of the system. The introduction explains the motivations and the goal of the work. Then, there is a brief survey of the HOOD hierarchical design method in the next point. It states as the base for the formalization method explained in the article. The notions of module, interface, operation, use and include relations are briefly explained. After it, the simple LOTOS language constructs are also presented. Next point explains the formalization of the HOOD structures. This is the most essentials part of the work where the method is presented on the exemplary HOOD diagram. LOTOS code is produced relate to the HOOD informal semantic. It expresses the main concepts of the HOOD dynamic model. There are the conclusions and further works proposals at the end of the article.
5
Content available Bezpieczna platforma sprzętowa dla aplikacji opisanych w języku FBD
Śnieżek M.
Pomiary Automatyka Kontrola
|
2005
|
R. 51, nr 1
31-33
PL
W pracy przedstawiono programowalny sterownik logiczny, zachowujący się w sposób bezpieczny. Zachowanie to obejmuje normalną pracę, podczas której wymaga się poprawnego sterowania, jak również stan awarii, w którym wyjścia muszą być automatycznie wyzerowane. Algorytm sterowania jest opisany metodą bloków funkcyjnych FBD i SFC zgodną z normą IEC-61131. Zastosowana architektura sprzętowa sprzyja podzieleniu oprogramowania na dwie części. Pierwsza część - stała, niezależna od aplikacji - obejmuje bibliotekę bloków funkcyjnych. część druga - zmienna, bezpośrednio zależna od aplikacji - zawiera strukturę połączeń bloków. Obydwie części są wykonywane przez osobne procesory. Do badania poprawności stałej części programu zaproponowano formalną metodę wykorzystującą logikę wyższego rzędu HOL. Część zamienną bada się stosując metodę zróżnicowanej retranslacji.
EN
To architecturally support the programming of safety related control applications in the graphical language Function Block Diagram and the verification of such software meeting the requirements of safety Integrity level 3, a dedicated, low complexity execution platform is presented. Its hardware is fault detecting to immediately initiate emegrency shut-downs in case of malfunctions. By design, there is no semantic gap between the programming and machine execution levels, enabling the safety licensing of application software by extremely simple, but rigorous methods, viz., diverse back translation and inspection. Operating in strictly periodic fashion, the platform exhibits fully predictable real time behaviour.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.