Wyniki wyszukiwania - BazTech

1

Software requirements elaboration with decision tables

Grzybowski Michał, Młyńczak Jakub, Sokołowska Lucyna, Matowicki Michał

Zeszyty Naukowe. Transport / Politechnika Śląska

|

2024

|

z. 125

89--99

EN

The paper describes decision table notation as a requirements definition technique. Modern critical systems, e.g., railway signaling systems, are implemented with electronic technologies. The use of computers in these systems has greatly expanded their functionality. Increase in functionality unfortunately leads to increase in complexity, which forces the designer to follow a more rigorous development process. The paper discusses the subject of describing expected software behavior, i.e., software requirements specification. It presents desired requirements features and describes how these features can be obtained by use of decision tables. The paper also discusses decision table transformations, which can reduce the effort to establish decision tables and facilitate their analysis. The authors’ experiments support the use of decision tables as a mean to increase requirements quality by providing tools for automatic decision table processing.

2

Detection of ladder program unstable states

Grzybowski Michał, Młyńczak Jakub, Folęga Piotr, Sokołowska Lucyna, Pietruszczak Daniel

Transport Problems

|

2024

|

T. 19, z. 3

107--119

EN

This paper presents a modern method of detecting unstable states in ladder programs. Ladder programs are standard formalism used in a wide range of automation applications, especially in railway signaling systems. This formalism is characterized by a lack of explicit program control flow, which can result in the presence of unstable states. A state is unstable, if it leads to cyclic state transitions not anticipated by the designer (loop). The presence of unstable states is one of the possible program defects. This kind of defect is hard to detect and can harm program reliability. The presence of unstable states can be verified with formal methods by the construction of a ladder program model and analysis of its properties. The authors propose a method of static analysis of ladder programs by translating them into predicate logic formulas and construction of formulas expression stability of the program, which can be analyzed with SAT solvers. The presented method allows for automatic verification of the presence of unstable states in the program. The method is conservative (i.e., it concludes that the program has no unstable states only if it is the case). Preliminary experiments performed by authors with a Z3 solver indicate that the method is suitable for use for verification of interlocking programs of computer-based railway signaling systems.

3

Description of route dependencies for computer-based railway signalling systems

Grzybowski Michał, Młyńczak Jakub, Sokołowska Lucyna

Archives of Transport

|

2024

|

Vol. 72, iss. 4

167--180

EN

Efficient and safe movement of trains on railway lines is assured by railway signalling systems. These systems assure safety of railway transport by preservation of dependencies. A significant fraction of dependencies is related to route setting, i.e., preparation of train travel through the specified running paths. The use of computer technology in modern systems allows for greater functionality and smaller physical devices dimension than older types of systems. This results in increased complexity of track layout and increased area of a single interlocking. Systems with considerable number of routes, over a thousand are becoming increasingly common. The research is concerned with the problem of describing route dependencies in computer-based interlocking configuration. During the research existing solutions have been analyzed and a method of describing route dependencies based on requirements of PKP PLK has been proposed. The proposed solution has been verified by functional testing of prototype interlocking. During the research, a formalism for describing the route has been devised, which allows for dependency realization by track layout independent computer program. In addition, during research algorithms for automatic verification of conflicting route exclusion correctness have been designed, which allows for reduction of effort required for verification of conflicting route exclusion function. The proposed method of describing route dependencies allows for simplification of inter-locking design and for automation of application data preparation. The method of implementing dependencies also allows for automation of conflicting route exclusion function verification, which decreased the effort required for verification activities while maintaining the high-quality standards.