3_2

\documentclass[a4paper,11pt]{article}
\usepackage[polish]{babel}
\usepackage[utf8]{inputenc}   % lub utf8
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{anysize}
\usepackage{enumerate}
\usepackage{times}
\usepackage{subfig}
\usepackage{cite}
%\marginsize{left}{right}{top}{bottom}
\marginsize{3cm}{3cm}{3cm}{3cm}



\begin{document}
\bibliographystyle{plain}
Z każdym działającym systemem komputerowym powiązane jest oczekiwanie
{\em poprawności} jego działania (\cite{Sommerville:2006:SE:1196763}). Istnieje szeroka
klasa systemów, dla których poprawność powiązana jest nie tylko z
wynikami ich pracy, ale również z~czasem, w~jakim wyniki te są
otrzymywane. Systemy takie nazywane są {\em systemami czasu
rzeczywistego}, a~ponieważ są one rozpatrywane  w~kontekście swojego
otoczenia, często określane są terminem {\em systemy wbudowane}
(\cite{Sommerville:2006:SE:1196763}, \cite{Szmuc:2010:MFwIOSCR}).

Ze względu na specyficzne cechy takich systemów, weryfikacja jakości
tworzonego oprogramowania oparta wyłącznie na jego testach jest
niewystarczająca. Coraz częściej w~takich sytuacjach, weryfikacja
poprawności tworzonego systemu lub najbardziej istotnych jego
modułów prowadzona jest z~zastosowaniem metod formalnych
(\cite{Alur:1990:AMR:90397.90438}, \cite{Szmuc:2010:MFwIOSCR}).


\bibliography{bibliografia}{}
\end{document}